Let x0 of type ο be given.
Apply xm with
x0,
0 ∈ If_i x0 1 0 ⟶ x0 leaving 2 subgoals.
Assume H0: x0.
Assume H1:
0 ∈ If_i x0 1 0.
The subproof is completed by applying H0.
Apply If_i_0 with
x0,
1,
0,
λ x1 x2 . 0 ∈ x2 ⟶ x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: 0 ∈ 0.
Apply FalseE with
x0.
Apply EmptyE with
0.
The subproof is completed by applying H1.