Proofgold Proposition

∀ x0 x1 x2 x3 x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x5 x6 x7 x8 x9 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ ChurchNum_8ary_proj_p x6 ⟶ ChurchNum_8ary_proj_p x7 ⟶ ChurchNum_8ary_proj_p x8 ⟶ ChurchNum_8ary_proj_p x9 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x1 x6 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x2 x7 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x2 x7 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x3 x8 x4 x9 = λ x11 x12 . x12) ⟶ ∀ x10 . (∀ x11 . x11 ∈ u5 ⟶ ∀ x12 . x12 ∈ u5 ⟶ ap (ap x10 x11) x12 ∈ 24) ⟶ (∀ x11 . x11 ∈ u5 ⟶ ∀ x12 . x12 ∈ u5 ⟶ ∀ x13 . x13 ∈ u5 ⟶ ap (ap x10 x11) x12 = ap (ap x10 x11) x13 ⟶ x12 = x13) ⟶ (∀ 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) ⟶ False

type
prop

theory
HotG

name
-

proof
PUUX7..

Megalodon
-

proofgold address
TMHPF..

creator
18893 Pr4zB../c7c4b..

owner
18893 Pr4zB../c7c4b..

term root
0ae8d..