Proofgold Object

λ x0 x1 . λ x2 : ι → ι . nat_primrec 1 (λ x3 x4 . If_i (x3 ∈ x0) 1 (mul_CSNo (x2 x3) x4)) (ordsucc x1)

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

theory
HotG

name
Prod

definition
PUL9u..

Megalodon
Prod

proofgold address
TMSX8..^Prod

creator
4970 Pr6Pc../cd98f..

owner
4970 Pr6Pc../cd98f..

term root
db3d3..