Proofgold Object

λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . In_rec_iii (λ x2 . λ x3 : ι → ι → ι → ι . If_iii (ordinal x2) (λ x4 . If_ii (x4 ∈ SNoS_ (ordsucc x2)) (x0 x4 (λ x5 . x3 (SNoLev x5) x5)) (Descr_ii (λ x5 : ι → ι . True))) (λ x4 . Descr_ii (λ x5 : ι → ι . True))) (SNoLev x1) x1

type
(ι → (ι → ι → ι) → ι → ι) → ι → ι → ι

theory
HotG

name
SNo_rec_ii

definition
PUK1b..

Megalodon
SNo_rec_ii

proofgold address
TMSBX..^SNo_rec_ii

creator
4949 Pr6Pc../7d90e..

owner
4949 Pr6Pc../7d90e..

term root
e148e..