Russell's paradox in Idris2

Russell.idr

%default total

-- A set is an index type, and a set for each index, inductively.
record Set where
  constructor MkSet
  i : Type
  f : i -> Set

-- Set `a` is contained in set `b` if there is an index in `b` at which we find
-- a set equal to `a`
In : Set -> Set -> Type
a `In` (MkSet i f) = (x : i ** a = f x)

-- The set of all sets that do not contain themselves
R : Set
R = MkSet (m : Set ** Not (m `In` m)) fst

-- R does not contain itself
R_not_in_R : Not (R `In` R)
R_not_in_R r_in_r@((.(R) ** r_not_in_r) ** Refl) = r_not_in_r r_in_r

-- Contradiction!
russell : Void
russell = R_not_in_R ((R ** R_not_in_R) ** Refl)