Proofgold Proposition

∀ x0 x1 x2 . SNoLt x0 x1 ⟶ SNo x1 ⟶ SNoLev x1 = x2 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ and (and (SNo x1) (SNoLev x1 ∈ SNoLev x0)) (SNoLt x0 x1)

type
prop

theory
HotG

name
-

proof
PURzn..

Megalodon
Conj_SNo_etaE__5__1

proofgold address
TMMQB..^{Conj_SNo_etaE__5__1}

creator
35045 PrNpY../cf40d..

owner
35047 PrNpY../aecab..

term root
a9d1b..