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

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

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

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

Assume H0: ChurchNum_3ary_proj_p x0.

Assume H1: ChurchNum_8ary_proj_p x2.

Assume H2: ChurchNum_3ary_proj_p x1.

Assume H3: ChurchNum_8ary_proj_p x3.

Apply H0 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 = (λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x6 x7 x8 : (ι → ι) → ι → ι . x5 x8 x6 x7) x1 ⟶ ChurchNums_3x8_to_u24 x4 x2 = ChurchNums_3x8_to_u24 x1 x3 ⟶ ∀ x5 : ο . x5 leaving 3 subgoals.

Apply H2 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) = (λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x6 x7 x8 : (ι → ι) → ι → ι . x5 x8 x6 x7) x4 ⟶ ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) x2 = ChurchNums_3x8_to_u24 x4 x3 ⟶ ∀ x5 : ο . x5 leaving 3 subgoals.

Assume H4: (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x6.

Apply FalseE with ChurchNums_3x8_to_u24 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) x2 = ChurchNums_3x8_to_u24 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) x3 ⟶ ∀ x4 : ο . x4.

Apply neq_0_1.

Apply H4 with λ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x5 (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . x6) ordsucc 0 = (λ x6 x7 x8 : (ι → ι) → ι → ι . x8) (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . x6) ordsucc 0.

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

Assume H5: x4 ((λ x5 x6 x7 : (ι → ι) → ι → ι . x7) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) ordsucc 0) ((λ x5 x6 x7 : (ι → ι) → ι → ι . x7) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) ordsucc 0).

The subproof is completed by applying H5.

Apply H1 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) = (λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x6 x7 x8 : (ι → ι) → ι → ι . x5 x8 x6 x7) (λ x5 x6 x7 : (ι → ι) → ι → ι . x6) ⟶ ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) x4 = ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x6) x3 ⟶ ∀ x5 : ο . x5 leaving 8 subgoals.

Apply H3 with λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) = (λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x6 x7 x8 : (ι → ι) → ι → ι . x5 x8 x6 x7) (λ x5 x6 x7 : (ι → ι) → ι → ι . x6) ⟶ ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) = ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x6) x4 ⟶ ∀ x5 : ο . x5 leaving 8 subgoals.

Assume H4: (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = (λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x5 x6 x7 : (ι → ι) → ι → ι . x4 x7 x5 x6) (λ x4 x5 x6 : (ι → ι) → ι → ι . x5).

Assume H5: ChurchNums_3x8_to_u24 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) = ChurchNums_3x8_to_u24 (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4).

Apply neq_8_0.

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

The subproof is completed by applying H5 with λ x5 x6 . x4 x6 x5.

Apply neq_9_0.

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

The subproof is completed by applying H5 with λ x5 x6 . x4 x6 x5.

Apply unknownprop_871e92d1e015b90191f05be741b9ed2cc4491066cf0bf7b2d76c5d141ce801a4.

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

The subproof is completed by applying H5 with λ x5 x6 . x4 x6 x5.

Assume H4: ... = ....

...

■

Proofgold Proof