Proofgold Proposition

∀ x0 . SNo x0 ⟶ ∀ x1 : ο . (ordinal (SNoLev x0) ⟶ SNo_ (SNoLev x0) x0 ⟶ x1) ⟶ x1

type
prop

theory
HF

name
-

proof
PUQ8e..

Megalodon
SNoLev_prop_impred

proofgold address
TMQF6..^{SNoLev_prop_impred}

creator
2357 PrGxv../e1e7c..

owner
2357 PrGxv../e1e7c..

term root
97c7d..