Proofgold Term Root Disambiguation

∀ x0 x1 . SNoCutP x0 x1 ⟶ (∀ x2 . x2 ∈ x0 ⟶ minus_SNo (minus_SNo x2) = x2) ⟶ (∀ x2 . x2 ∈ x1 ⟶ minus_SNo (minus_SNo x2) = x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ SNo x2) ⟶ (∀ x2 . x2 ∈ x1 ⟶ SNo x2) ⟶ SNo (SNoCut x0 x1) ⟶ SNo (minus_SNo (minus_SNo (SNoCut x0 x1))) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev (minus_SNo (minus_SNo (SNoCut x0 x1)))) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) (minus_SNo (minus_SNo (SNoCut x0 x1)))) ⟶ minus_SNo (minus_SNo (SNoCut x0 x1)) = SNoCut x0 x1

as obj
-

as prop
59be3..^{Conj_minus_SNo_invol__5__6}

theory
HotG

stx
b740c..

address
TMPe4..^{Conj_minus_SNo_invol__5__6}