Proofgold Object

λ x0 . pack_u (setprod omega x0) (λ x1 . lam 2 (λ x2 . If_i (x2 = 0) (ordsucc (ap x1 0)) (ap x1 1)))

type
ι → ι

theory
HotG

name
-

definition
PUStC..

Megalodon
-

proofgold address
TMTBA..

creator
35044 PrHS6../41797..

owner
35044 PrHS6../41797..

term root
3a679..