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.

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

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

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

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

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

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

Assume H0: ChurchNum_3ary_proj_p x0.

Assume H1: ChurchNum_3ary_proj_p x1.

Assume H2: ChurchNum_3ary_proj_p x2.

Assume H3: ChurchNum_3ary_proj_p x3.

Assume H4: ChurchNum_3ary_proj_p x4.

Assume H5: ChurchNum_8ary_proj_p x5.

Assume H6: ChurchNum_8ary_proj_p x6.

Assume H7: ChurchNum_8ary_proj_p x7.

Assume H8: ChurchNum_8ary_proj_p x8.

Assume H9: ChurchNum_8ary_proj_p x9.

Assume H10: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x1 x6 = λ x10 x11 . x11.

Assume H11: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x2 x7 = λ x10 x11 . x11.

Assume H12: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x3 x8 = λ x10 x11 . x11.

Assume H13: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x4 x9 = λ x10 x11 . x11.

Assume H14: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x2 x7 = λ x10 x11 . x11.

Assume H15: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x3 x8 = λ x10 x11 . x11.

Assume H16: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x4 x9 = λ x10 x11 . x11.

Assume H17: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x3 x8 = λ x10 x11 . x11.

Assume H18: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x4 x9 = λ x10 x11 . x11.

Assume H19: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x3 x8 x4 x9 = λ x10 x11 . x11.

Let x10 of type ι be given.

Assume H20: ∀ x11 . x11 ∈ u5 ⟶ ∀ x12 . x12 ∈ u5 ⟶ ap (ap x10 x11) x12 ∈ 24.

Assume H21: ∀ x11 . x11 ∈ u5 ⟶ ∀ x12 . x12 ∈ u5 ⟶ ∀ x13 . x13 ∈ u5 ⟶ ap (ap x10 x11) x12 = ap (ap x10 x11) x13 ⟶ x12 = x13.

Assume H22: ∀ x11 . x11 ∈ u5 ⟶ ∀ x12 . x12 ∈ u5 ⟶ (x11 = x12 ⟶ ∀ x13 : ο . x13) ⟶ ∀ x13 . x13 ∈ u5 ⟶ ∀ x14 . x14 ∈ u5 ⟶ ap (ap x10 x11) x13 = ap (ap x10 x12) x14 ⟶ ∀ x15 : ο . x15.

Claim L23: ...

...

Claim L24: ...

...

Claim L25: atleastp (setprod u5 u5) u24

Let x11 of type ο be given.

Assume H25: ∀ x12 : ι → ι . inj (setprod u5 u5) u24 x12 ⟶ x11.

Apply H25 with λ x12 . ap (ap x10 (ap x12 0)) (ap x12 1).

Apply andI with ∀ x12 . x12 ∈ setprod u5 u5 ⟶ (λ x13 . ap (ap x10 (ap x13 0)) (ap x13 1)) x12 ∈ u24, ∀ x12 . ... ⟶ ∀ x13 . ... ⟶ (λ x14 . ap (ap x10 ...) ...) ... = ... ⟶ x12 = x13 leaving 2 subgoals.

...

Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with u24 leaving 2 subgoals.

The subproof is completed by applying unknownprop_a7f3578ada9cacf1cb3296f5290d2c691e8a6f96bb11bbe9193ef025e25fc69a.

Apply unknownprop_cb31ba5b53de7ed1501ccb7838b0596c4806363c08f052d879d991759ac7d059 with λ x11 x12 . atleastp x11 u24.

Apply atleastp_tra with mul_nat u5 u5, setprod u5 u5, u24 leaving 2 subgoals.

Apply equip_atleastp with mul_nat u5 u5, setprod u5 u5.

Apply unknownprop_0ff18b7eb504eb7c264f5ad42462c21af832d47f1fcbedf3de67bfbc10c7fdfc with u5, u5 leaving 2 subgoals.

The subproof is completed by applying nat_5.

The subproof is completed by applying L25.

■

Proofgold Proof