Apply unknownprop_9282c4fc031a36c9b2eafd476b3c98b0d2f015723908debe89fc7acd2c78f947 with
6,
λ x0 x1 . x1 = ChurchNum_ii_7 ChurchNum2 ordsucc 0 leaving 2 subgoals.
The subproof is completed by applying nat_6.
Apply unknownprop_180b0fd5c0d77d89fc7c74d0519e38ad47b1b50cde73428ffe5103966c8941b7 with
λ x0 x1 . add_nat (exp_nat 2 6) x1 = ChurchNum_ii_6 ChurchNum2 ordsucc (ChurchNum_ii_6 ChurchNum2 ordsucc 0).
Claim L0: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0
Let x2 of type ι → ο be given.
Apply unknownprop_1ecba3dd5eafa4f5c4681522469f6140788e091a78ad9f01e97cc0b6f2c0488f with
ordsucc,
nat_p,
λ x3 . add_nat (exp_nat 2 6) x3,
0,
λ x3 . x2 leaving 4 subgoals.
The subproof is completed by applying nat_ordsucc.
The subproof is completed by applying add_nat_SR with
exp_nat 2 6.
The subproof is completed by applying nat_0.
Let x2 of type ι → ι → ο be given.
Apply L0 with
λ x3 . x2 x3 y1 ⟶ x2 y1 x3.
Assume H1: x2 y1 y1.
The subproof is completed by applying H1.