Proofgold Object

λ x0 : ι → (ι → ι) → ι . λ x1 . In_rec_ii (λ x2 . λ x3 : ι → ι → ι . If_ii (ordinal x2) (λ x4 . If_i (x4 ∈ SNoS_ (ordsucc x2)) (x0 x4 (λ x5 . x3 (SNoLev x5) x5)) (prim0 (λ x5 . True))) (λ x4 . prim0 (λ x5 . True))) (SNoLev x1) x1

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

theory
HotG

name
SNo_rec_i

definition
PUK1b..

Megalodon
SNo_rec_i

proofgold address
TMFnU..^SNo_rec_i

creator
4949 Pr6Pc../0af53..

owner
4949 Pr6Pc../0af53..

term root
be45d..