Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ ∀ x1 . SNo x1 ⟶ ∀ x2 : ο . (SNo (mul_SNo x0 x1) ⟶ (∀ x3 . x3 ∈ SNoL x0 ⟶ ∀ x4 . x4 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4))) ⟶ (∀ x3 . x3 ∈ SNoR x0 ⟶ ∀ x4 . x4 ∈ SNoR x1 ⟶ SNoLt (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4))) ⟶ (∀ x3 . x3 ∈ SNoL x0 ⟶ ∀ x4 . x4 ∈ SNoR x1 ⟶ SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)) (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4))) ⟶ (∀ x3 . x3 ∈ SNoR x0 ⟶ ∀ x4 . x4 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x3 x4)) (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4))) ⟶ x2) ⟶ x2

as obj
-

as prop
5e4d1..^{mul_SNo_prop_1}

theory
HotG

stx
fd8fe..

address
TMdaG..^{mul_SNo_prop_1}