Apply unknownprop_9282c4fc031a36c9b2eafd476b3c98b0d2f015723908debe89fc7acd2c78f947 with 5, λ x0 x1 . x1 = ChurchNum_ii_6 ChurchNum2 ordsucc 0 leaving 2 subgoals.

The subproof is completed by applying nat_5.

Apply unknownprop_dfd75789bdcf74d855c762b087b060f27bac1d86daec67bb0564ef3cbdbd7473 with λ x0 x1 . add_nat (exp_nat 2 5) x1 = ChurchNum_ii_5 ChurchNum2 ordsucc (ChurchNum_ii_5 ChurchNum2 ordsucc 0).

set y0 to be add_nat (exp_nat 2 5) (ChurchNum_ii_5 ChurchNum2 ordsucc 0)

set y1 to be ChurchNum_ii_5 ChurchNum2 ordsucc (ChurchNum_ii_5 ChurchNum2 ordsucc 0)

Claim L0: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0

Let x2 of type ι → ο be given.

Assume H0: x2 (ChurchNum_ii_5 ChurchNum2 ordsucc (ChurchNum_ii_5 ChurchNum2 ordsucc 0)).

Apply unknownprop_3d492f63bbda05786f59e1a020a0f00cded12b012672cfcb59b4dfe595a76487 with ordsucc, nat_p, λ x3 . add_nat (exp_nat 2 5) 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 5.

The subproof is completed by applying nat_0.

Apply add_nat_0R with exp_nat 2 5, λ x3 x4 . ChurchNum_ii_5 ChurchNum2 ordsucc x4 = ChurchNum_ii_5 ChurchNum2 ordsucc (ChurchNum_ii_5 ChurchNum2 ordsucc 0), λ x3 . x2 leaving 2 subgoals.

Apply unknownprop_8e67f22739f9a01fd2d9438edd2f3f6d8d323d1fa4d050bc09f5b1af8d3b6dd7 with λ x3 x4 . ChurchNum_ii_5 ChurchNum2 ordsucc x4 = ChurchNum_ii_5 ChurchNum2 ordsucc (ChurchNum_ii_5 ChurchNum2 ordsucc 0).

Let x3 of type ι → ι → ο be given.

Assume H1: x3 (ChurchNum_ii_5 ChurchNum2 ordsucc 32) (ChurchNum_ii_5 ChurchNum2 ordsucc (ChurchNum_ii_5 ChurchNum2 ordsucc 0)).

The subproof is completed by applying H1.

The subproof is completed by applying H0.

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.

■

Proofgold Proof