Proofgold Proposition

(∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x1 ∈ ordsucc (SNoLev x2) ⟶ x2 = minus_SNo x3 ⟶ 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
TMNXk..

creator
35087 PrNpY../36ba2..

owner
35087 PrNpY../36ba2..

term root
2c724..