Let x0 of type ι be given.
Apply nat_inv with
x0,
or (x0 = 0) (x0 = 1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying orIL with x0 = 0, x0 = 1.
Apply H2 with
or (x0 = 0) (x0 = 1).
Let x1 of type ι be given.
Apply H3 with
or (x0 = 0) (x0 = 1).
Apply unknownprop_2da221bcdd2314e7a8865e1e89957a529238abd39a22657b0cdfc26f16078944 with
x0,
x1,
or (x0 = 0) (x0 = 1) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply unknownprop_b680053007d2079a50fc651be9018eecbfbee9dc8c41a96ffea48406193e0e98 with
x1,
mul_nat x0 x1 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply mul_nat_p with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply ordsucc_inj with
x1,
add_nat x1 (mul_nat x0 x1).
Apply H5 with
λ x2 x3 . x2 = ordsucc (add_nat x1 (mul_nat x0 x1)).
Apply add_nat_SL with
x1,
mul_nat x0 x1,
λ x2 x3 . x0 = x2 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply mul_nat_p with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply H5 with
λ x2 x3 . x0 = add_nat x2 (mul_nat x0 x1).
Apply mul_nat_SR with
x0,
x1,
λ x2 x3 . x0 = x2 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply H5 with
λ x2 x3 . x0 = mul_nat x0 x2.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H1 with λ x3 x4 . x2 x4 x3.
Assume H6: x0 = 0.
Apply FalseE with
or (x0 = 0) (x0 = 1).
Apply EmptyE with
x1.
Apply H6 with
λ x2 x3 . x1 ∈ x2.
Apply H5 with
λ x2 x3 . x1 ∈ x3.
The subproof is completed by applying ordsuccI2 with x1.
Assume H6: x1 = 0.
Apply orIR with
x0 = 0,
x0 = 1.
Apply H5 with
λ x2 x3 . x3 = 1.
set y2 to be 1
Claim L7:
∀ x3 : ι → ο . x3 y2 ⟶ x3 (ordsucc x1)Let x3 of type ι → ο be given.
The subproof is completed by applying H6 with
λ x4 x5 . (λ x6 . x3) (ordsucc x4) (ordsucc x5).
Let x3 of type ι → ι → ο be given.
Apply L7 with
λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H8: x3 y2 y2.
The subproof is completed by applying H8.