Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ mul_SNo 2 x0 = add_SNo (mul_SNo 2 x1) 1 ⟶ ∀ x2 : ο . x2

as obj
-

as prop
af26f..^{not_eq_2m_2n1}

theory
HotG

stx
afc5a..

address
TMGpp..^{not_eq_2m_2n1}