Let x0 of type ι be given.
Assume H1: 1 ∈ x0.
Apply SingE with
Sing 1,
Sing x0,
λ x1 x2 . 1 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying SingI with 1.
Apply In_irref with
1.
Apply SingE with
x0,
1,
λ x1 x2 . 1 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H1.