Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 x5 . SNo x2 ⟶ SNo x3 ⟶ SNoLt x3 x2 ⟶ SNoLt (add_SNo x2 (mul_SNo x4 x5)) (add_SNo x3 (mul_SNo x4 x5)) ⟶ SNoLt x2 x3 ⟶ SNoLt x3 (mul_SNo x0 x1)

as obj
-

as prop
3cff7..^{Conj_mul_SNo_SNoR_interpolate__4__3}

theory
HotG

stx
202df..