Proofgold Term Root Disambiguation

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

as obj
-

as prop
d1fff..^{mul_SNo_SNoR_interpolate_impred}

theory
HotG

stx
4a79b..

address
TMYf3..^{mul_SNo_SNoR_interpolate_impred}