Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . SNoCutP x0 x1 ⟶ SNoCutP x2 x3 ⟶ ∀ x4 x5 . x4 = SNoCut x0 x1 ⟶ x5 = SNoCut x2 x3 ⟶ ∀ x6 . x6 ∈ SNoR (mul_SNo x4 x5) ⟶ ∀ x7 : ο . (∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x3 ⟶ SNoLe (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x9)) (add_SNo x6 (mul_SNo x8 x9)) ⟶ x7) ⟶ (∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x2 ⟶ SNoLe (add_SNo (mul_SNo x8 x5) (mul_SNo x4 x9)) (add_SNo x6 (mul_SNo x8 x9)) ⟶ x7) ⟶ x7

as obj
-

as prop
a2323..^{mul_SNo_SNoCut_SNoR_interpolate_impred}

theory
HotG

stx
9a4a7..

address
TMFkW..^{mul_SNo_SNoCut_SNoR_interpolate_impred}