Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ (∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ and (and (and (SNo (minus_SNo x2)) (∀ x3 . x3 ∈ SNoL x2 ⟶ SNoLt (minus_SNo x2) (minus_SNo x3))) (∀ x3 . x3 ∈ SNoR x2 ⟶ SNoLt (minus_SNo x3) (minus_SNo x2))) (SNoCutP (prim5 (SNoR x2) minus_SNo) (prim5 (SNoL x2) minus_SNo))) ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ x1 ∈ SNoS_ (SNoLev x0) ⟶ and (and (SNo (minus_SNo x1)) (∀ x2 . x2 ∈ SNoL x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x2))) (∀ x2 . x2 ∈ SNoR x1 ⟶ SNoLt (minus_SNo x2) (minus_SNo x1))

type
prop

theory
HotG

name
-

proof
PURzn..

Megalodon
Conj_minus_SNo_prop1__2__2

proofgold address
TMYMa..^{Conj_minus_SNo_prop1__2__2}

creator
35045 PrNpY../41c27..

owner
35047 PrNpY../be82e..

term root
02f59..