Proofgold Term Root Disambiguation

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

as obj
-

as prop
39d66..

theory
HotG

stx
ddad9..

address
TMZex..