Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_SNo x0 x0 = mul_SNo 2 (mul_SNo x1 x1) ⟶ x1 = 0

as obj
-

as prop
9bd18..^{form100_1_lem1}

theory
HotG

stx
afc5a..

address
TMbgN..^{form100_1_lem1}