Proofgold Proposition

∀ 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

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_minus_SNo_invol__8__2

proofgold address
TMXse..^{Conj_minus_SNo_invol__8__2}

creator
35053 PrNpY../4ce5e..

owner
35061 PrNpY../adc41..

term root
1195c..