Proofgold Term Root Disambiguation

∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ add_SNo x0 x1 = u12 ⟶ add_SNo x0 (mul_SNo 2 x1) = u20 ⟶ and (x0 = u4) (x1 = u8)

as obj
-

as prop
f7ea8..

theory
HotG

stx
62a5c..

address
TMa7H..