Proofgold Object

λ x0 . PSNo (ordsucc (SNoLev x0)) (λ x1 . and (x1 ∈ x0) (x1 = SNoLev x0 ⟶ ∀ x2 : ο . x2))

type
ι → ι

theory
HotG

name
SNo_extend0

definition
PUUwp..

Megalodon
SNo_extend0

proofgold address
TMbS5..^SNo_extend0

creator
4910 Pr6Pc../a6634..

owner
4910 Pr6Pc../a6634..

term root
997d9..