Apply unknownprop_9282c4fc031a36c9b2eafd476b3c98b0d2f015723908debe89fc7acd2c78f947 with
7,
λ x0 x1 . x1 = ChurchNum_ii_8 ChurchNum2 ordsucc 0 leaving 2 subgoals.
The subproof is completed by applying nat_7.
Apply unknownprop_6df9254739f4a388867a5d36973fd227e06018cecfed76efdc871bfcb7b2c526 with
λ x0 x1 . add_nat (exp_nat 2 7) x1 = ChurchNum_ii_7 ChurchNum2 ordsucc (ChurchNum_ii_7 ChurchNum2 ordsucc 0).
Claim L0: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0
Let x2 of type ι → ο be given.
Apply unknownprop_90ee732e350e6ffe2073d662ad885e0f4d56a79b3cc64afadf949a48ec2985f2 with
ordsucc,
nat_p,
λ x3 . add_nat (exp_nat 2 7) 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 7.
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.