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 x7 x5 x6) ⟶ ChurchNums_3x8_to_u24 x0 x2 = ChurchNums_3x8_to_u24 x1 x3 ⟶ ∀ x4 : ο . x4

type
prop

theory
HotG

name
-

proof
PULQa..

Megalodon
-

proofgold address
TMNiv..

creator
18790 Pr4zB../9e459..

owner
18790 Pr4zB../9e459..

term root
a9635..