Proofgold Term Root Disambiguation

∀ 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) ⟶ minus_SNo (minus_SNo (SNoCut x0 x1)) = SNoCut x0 x1

as obj
-

as prop
687fa..^{Conj_minus_SNo_invol__8__0}

theory
HotG

stx
b740c..

address
TMFyo..^{Conj_minus_SNo_invol__8__0}