Proofgold Proposition

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

type
prop

theory
HotG

name
-

proof
PUfqD..

Megalodon
-

proofgold address
TMbDB..

creator
11516 PrEBh../7833b..

owner
11516 PrEBh../7833b..

term root
8a66e..