Proofgold Object

λ x0 . PSNo (ordsucc (SNoLev x0)) (λ x1 . or (x1 ∈ x0) (x1 = SNoLev x0))

type
ι → ι

theory
HotG

name
SNo_extend1

definition
PUUwp..

Megalodon
SNo_extend1

proofgold address
TMQVo..^SNo_extend1

creator
4910 Pr6Pc../44c47..

owner
4910 Pr6Pc../44c47..

term root
464e4..