Proofgold Object

λ x0 x1 . unpack_p_i x0 (λ x2 . λ x3 : ι → ο . unpack_p_i x1 (λ x4 . λ x5 : ι → ο . pack_p (setexp x4 x2) (λ x6 . ∀ x7 . x7 ∈ x2 ⟶ x3 x7 ⟶ x5 (ap x6 x7))))

type
ι → ι → ι

theory
HotG

name
-

definition
PUfqD..

Megalodon
-

proofgold address
TMU6d..

creator
11516 PrEBh../c3a84..

owner
11516 PrEBh../c3a84..

term root
3f5e4..