Proofgold Proposition

∀ x0 x1 x2 . SNo x0 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 x5 . SNoCutP x4 x5 ⟶ x3 = SNoCut x4 x5 ⟶ minus_SNo x3 = SNoCut (prim5 x5 minus_SNo) (prim5 x4 minus_SNo)) ⟶ SNoCutP x1 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ SNo x3) ⟶ x0 = SNoCut x1 x2 ⟶ SNo (SNoCut x1 x2) ⟶ minus_SNo x0 = SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_minus_SNoCut_eq_lem__11__3

proofgold address
TMKGQ..^{Conj_minus_SNoCut_eq_lem__11__3}

creator
35053 PrNpY../3df4c..

owner
35061 PrNpY../5e936..

term root
30015..