Proofgold Proposition

∀ 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

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_minus_SNo_invol__8__0

proofgold address
TMHW2..^{Conj_minus_SNo_invol__8__0}

creator
35053 PrNpY../ac6ff..

owner
35061 PrNpY../09030..

term root
138f4..