Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Claim L0: ChurchNums_8_perm_6_7_0_1_2_3_4_5 x0 = (λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x1 x8 x9 x2 x3 x4 x5 x6 x7) x0

Let x1 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.

Assume H0: x1 (ChurchNums_8_perm_6_7_0_1_2_3_4_5 x0) ((λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x2 x9 x10 x3 x4 x5 x6 x7 x8) x0).

The subproof is completed by applying H0.

Apply L0 with λ x1 x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2 = x0.

Assume H1: x1 (ChurchNums_8_perm_2_3_4_5_6_7_0_1 ((λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x2 x9 x10 x3 x4 x5 x6 x7 x8) x0)) x0.

The subproof is completed by applying H1.

■

Proofgold Proof