| pf |
|---|
Apply nat_ind with λ x0 . ∀ x1 . nat_p x1 ⟶ ordsucc x1 = add_nat x0 x0 ⟶ or (x0 ∈ x1) (and (x1 = 1) (x0 = 1)) leaving 2 subgoals.
Let x0 of type ι be given.
Apply add_nat_0R with 0, λ x1 x2 . ordsucc x0 = x2 ⟶ or (0 ∈ x0) (and (x0 = 1) (0 = 1)).
Apply FalseE with or (0 ∈ x0) (and (x0 = 1) (0 = 1)).
Apply neq_ordsucc_0 with x0.
The subproof is completed by applying H1.
Let x0 of type ι be given.
Apply add_nat_SR with ordsucc x0, x0, λ x1 x2 . ∀ x3 . nat_p x3 ⟶ ordsucc x3 = x2 ⟶ or (ordsucc x0 ∈ x3) (and (x3 = 1) (ordsucc x0 = 1)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_nat_SL with x0, x0, λ x1 x2 . ∀ x3 . nat_p x3 ⟶ ordsucc x3 = ordsucc x2 ⟶ or (ordsucc x0 ∈ x3) (and (x3 = 1) (ordsucc x0 = 1)) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Apply unknownprop_b35032c81ea06ad673f8a0490d5be4e7b984453ec9378fed4adde429c2b88d75 with λ x1 . ordsucc x1 = ordsucc (ordsucc (add_nat x0 x0)) ⟶ or (ordsucc x0 ∈ x1) (and (x1 = 1) (ordsucc x0 = 1)) leaving 3 subgoals.
Apply FalseE with or (ordsucc x0 ∈ 0) (and (0 = 1) (ordsucc x0 = 1)).
Apply neq_0_ordsucc with add_nat x0 x0.
Apply ordsucc_inj with 0, ordsucc (add_nat x0 x0).
The subproof is completed by applying H2.
Apply orIR with ordsucc x0 ∈ 1, and (1 = 1) (ordsucc x0 = 1).
Apply andI with 1 = 1, ordsucc x0 = 1 leaving 2 subgoals.
set y1 to be 1
Let x2 of type ι → ι → ο be given.
Assume H3: x2 y1 y1.
The subproof is completed by applying H3.
Apply nat_inv with x0, ordsucc x0 = 1 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H3: x0 = 0.
Apply H3 with λ x1 x2 . ordsucc x2 = 1.
set y1 to be 1
Let x2 of type ι → ι → ο be given.
Assume H4: x2 y1 y1.
The subproof is completed by applying H4.
Apply H3 with ordsucc x0 = 1.
Let x1 of type ι be given.
Apply H4 with ordsucc x0 = 1.
Apply FalseE with ordsucc x0 = 1.
Apply neq_0_ordsucc with add_nat ... ....
■ |
|