Proofgold Proposition

∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 . PreContinuousHom (pack_c x0 x2) (pack_c x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ x7 ∈ x1) ⟶ x3 x6 ⟶ x2 (λ x7 . and (x7 ∈ x0) (x6 (ap x4 x7))))

type
prop

theory
HotG

name
-

proof
PUdXV..

Megalodon
Hom_struct_c_pack

proofgold address
TMcGM..^{Hom_struct_c_pack}

creator
9630 PrCx1../78dfa..

owner
9630 PrCx1../78dfa..

term root
14794..