Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ setminus omega 1 ⟶ mul_SNo x0 x0 = mul_SNo 2 (mul_SNo x1 x1) ⟶ ∀ x2 : ο . x2

as obj
-

as prop
1129e..^{form100_1_lem2}

theory
HotG

stx
afc5a..

address
TMTQV..^{form100_1_lem2}