Proofgold Term Root Disambiguation

∀ x0 x1 . SNoCutP x0 x1 ⟶ (∀ x2 . x2 ∈ x0 ⟶ minus_SNo (minus_SNo x2) = x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ SNo x2) ⟶ (∀ x2 . x2 ∈ x1 ⟶ SNo x2) ⟶ SNo (SNoCut x0 x1) ⟶ minus_SNo (minus_SNo (SNoCut x0 x1)) = SNoCut x0 x1

as obj
-

as prop
a064b..^{Conj_minus_SNo_invol__8__2}

theory
HotG

stx
b740c..

address
TMTSJ..^{Conj_minus_SNo_invol__8__2}