Proofgold Object

λ x0 x1 . unpack_u_i x0 (λ x2 . λ x3 : ι → ι . unpack_u_i x1 (λ x4 . λ x5 : ι → ι . pack_u (setprod x2 x4) (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (x3 (ap x6 0)) (x5 (ap x6 1))))))

type
ι → ι → ι

theory
HotG

name
-

definition
PUYhi..

Megalodon
-

proofgold address
TMSwY..

creator
11768 PrEBh../e5b3c..

owner
11768 PrEBh../e5b3c..

term root
86f6b..