Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ and (and (and (SNo (minus_SNo x0)) (∀ x1 . x1 ∈ SNoL x0 ⟶ SNoLt (minus_SNo x0) (minus_SNo x1))) (∀ x1 . x1 ∈ SNoR x0 ⟶ SNoLt (minus_SNo x1) (minus_SNo x0))) (SNoCutP (prim5 (SNoR x0) minus_SNo) (prim5 (SNoL x0) minus_SNo))

as obj
-

as prop
f0b75..^{minus_SNo_prop1}

theory
HotG

stx
2cf07..

address
TMPFD..^{minus_SNo_prop1}