Apply nat_inv_impred with
λ x0 . x0 ⊆ 2 ⟶ or (or (x0 = 0) (x0 = 1)) (x0 = 2) leaving 2 subgoals.
Assume H0: 0 ⊆ 2.
Apply orIL with
or (0 = 0) (0 = 1),
0 = 2.
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 ⊆ 2 ⟶ or (or (ordsucc x0 = 0) (ordsucc x0 = 1)) (ordsucc x0 = 2) leaving 2 subgoals.
Assume H0: 1 ⊆ 2.
Apply orIL with
or (1 = 0) (1 = 1),
1 = 2.
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.
Apply nat_inv_impred with
λ x0 . ordsucc (ordsucc x0) ⊆ 2 ⟶ or (or (ordsucc (ordsucc x0) = 0) (ordsucc (ordsucc x0) = 1)) (ordsucc (ordsucc x0) = 2) leaving 2 subgoals.
Assume H0: 2 ⊆ 2.
Apply orIR with
or (2 = 0) (2 = 1),
2 = 2.
set y0 to be 2
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 (or (ordsucc (ordsucc (ordsucc x0)) = 0) (ordsucc (ordsucc (ordsucc x0)) = 1)) (ordsucc (ordsucc (ordsucc x0)) = 2).
Apply In_irref with
2.
Apply H1 with
2.
Apply nat_ordsucc_in_ordsucc with
ordsucc (ordsucc x0),
1 leaving 2 subgoals.
Apply nat_ordsucc with
ordsucc x0.
Apply nat_ordsucc with
x0.
The subproof is completed by applying H0.
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.