Proofgold Object

λ x0 : ι → ι → (ι → ι → ι) → ι . SNo_rec_ii (λ x1 . λ x2 : ι → ι → ι . λ x3 . If_i (SNo x3) (SNo_rec_i (λ x4 . λ x5 : ι → ι . x0 x1 x4 (λ x6 x7 . If_i (x6 = x1) (x5 x7) (x2 x6 x7))) x3) 0)

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

theory
HotG

name
SNo_rec2

definition
PUK1b..

Megalodon
SNo_rec2

proofgold address
TMaJ9..^SNo_rec2

creator
4949 Pr6Pc../5bb3a..

owner
4949 Pr6Pc../5bb3a..

term root
7d10a..