Proofgold Object

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

type
ι → ι → ι

theory
HotG

name
-

definition
PUdPp..

Megalodon
-

proofgold address
TMF1A..

creator
11767 PrEBh../a6f22..

owner
11767 PrEBh../a6f22..

term root
4a4f5..