Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoCutP (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} (prim5 (SNoL x1) (add_SNo x0))) (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} (prim5 (SNoR x1) (add_SNo x0)))

as obj
-

as prop
f86b1..^{add_SNo_SNoCutP}

theory
HotG

stx
7edd8..

address
TMdKu..^{add_SNo_SNoCutP}