Proofgold Proposition

(∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x2 = minus_SNo x3 ⟶ SNoLev x3 ∈ SNoLev x0 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev (minus_SNo x3)) ⟶ ordinal (ordsucc (SNoLev x2)) ⟶ x1 ∈ SNoLev x0) ⟶ ∀ x0 : ο . x0

type
prop

theory
HotG

name
-

proof
PUfXk..

Megalodon
-

proofgold address
TMagT..

creator
35087 PrNpY../6f7dc..

owner
35087 PrNpY../6f7dc..

term root
84cc6..