Apply nat_inv_impred with
λ x0 . x0 ⊆ 1 ⟶ or (x0 = 0) (x0 = 1) leaving 2 subgoals.
Assume H0: 0 ⊆ 1.
Apply orIL with
0 = 0,
0 = 1.
Let x0 of type ι → ι → ο be given.
Assume H1: x0 0 0.
The subproof is completed by applying H1.
Apply nat_inv_impred with
λ x0 . ordsucc x0 ⊆ 1 ⟶ or (ordsucc x0 = 0) (ordsucc x0 = 1) leaving 2 subgoals.
Assume H0: 1 ⊆ 1.
Apply orIR with
1 = 0,
1 = 1.
set y0 to be 1
Let x1 of type ι → ι → ο be given.
Assume H1: x1 y0 y0.
The subproof is completed by applying H1.
Let x0 of type ι be given.
Apply FalseE with
or (ordsucc (ordsucc x0) = 0) (ordsucc (ordsucc x0) = 1).
Apply In_irref with
1.
Apply H1 with
1.
Apply nat_ordsucc_in_ordsucc with
ordsucc x0,
0 leaving 2 subgoals.
Apply nat_ordsucc with
x0.
The subproof is completed by applying H0.
Apply nat_0_in_ordsucc with
x0.
The subproof is completed by applying H0.