Proofgold Proposition

∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_8ary_proj_p x3 ⟶ (x0 = λ x5 x6 x7 : (ι → ι) → ι → ι . x1 x6 x7 x5) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt6_id_ge6_rot2 x2 x0) (ChurchNums_8_perm_2_3_4_5_6_7_0_1 x2) = ChurchNums_3x8_to_u24 x1 x3 ⟶ ∀ x4 : ο . x4

type
prop

theory
HotG

name
-

proof
PUZ45..

Megalodon
-

proofgold address
TMKN6..

creator
18850 Pr4zB../dcd8e..

owner
18850 Pr4zB../dcd8e..

term root
e1395..