Proofgold Proposition

∀ x0 : (ι → ι) → ι → ι . ChurchNum_p x0 ⟶ ∀ x1 : (ι → ι) → ι → ι . ChurchNum_p x1 ⟶ x0 ordsucc (x1 ordsucc 0) = add_nat (x0 ordsucc 0) (x1 ordsucc 0)

type
prop

theory
HotG

name
-

proof
PUSRF..

Megalodon
-

proofgold address
TMG33..

creator
18726 Pr4zB../eb5f7..

owner
18726 Pr4zB../eb5f7..

term root
566d9..