Proofgold Object

λ x0 x1 . unpack_r_i x0 (λ x2 . λ x3 : ι → ι → ο . unpack_r_i x1 (λ x4 . λ x5 : ι → ι → ο . pack_r (setexp x4 x2) (λ x6 x7 . ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x2 ⟶ x3 x8 x9 ⟶ x5 (ap x6 x8) (ap x7 x9))))

type
ι → ι → ι

theory
HotG

name
BinReln_exp

definition
PUKcr..

Megalodon
-

proofgold address
TMGxk..

creator
11519 PrEBh../9e8bb..

owner
11519 PrEBh../9e8bb..

term root
98649..