Proofgold Proposition

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

type
prop

theory
HotG

name
-

proof
PUdXV..

Megalodon
Hom_struct_r_pack

proofgold address
TMSNp..^{Hom_struct_r_pack}

creator
9630 PrCx1../557ad..

owner
9630 PrCx1../557ad..

term root
4e486..