Proofgold Object

λ x0 . ∀ x1 : ι → ο . x1 0 ⟶ (∀ x2 . x1 x2 ⟶ x1 (ordsucc x2)) ⟶ x1 x0

type
ι → ο

theory
HotG

name
nat_p

definition
PUL8Q..

Megalodon
nat_p

proofgold address
TMQws..^nat_p

creator
4882 Pr6Pc../5dfc3..

owner
4882 Pr6Pc../5dfc3..

term root
458be..