Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo (add_SNo (mul_SNo x2 x1) (add_SNo (mul_SNo x0 x3) (minus_SNo (mul_SNo x2 x3))))

as obj
-

as prop
3a9ab..^{SNo_mul_SNo_lem}

theory
HotG

stx
0d8c8..

address
TMSxP..^{SNo_mul_SNo_lem}