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_lt5_id_ge5_rot2 x2 x0) (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x2) = ChurchNums_3x8_to_u24 x1 x3 ⟶ ∀ x4 : ο . x4

type
prop

theory
HotG

name
-

proof
PUX3W..

Megalodon
-

proofgold address
TMZk9..

creator
18840 Pr4zB../0e2cf..

owner
18840 Pr4zB../0e2cf..

term root
9d122..