Proofgold Proposition

∀ x0 x1 x2 x3 x4 . PtdSetHom (pack_e x0 x2) (pack_e x1 x3) x4 = and (x4 ∈ setexp x1 x0) (ap x4 x2 = x3)

type
prop

theory
HotG

name
-

proof
PUdXV..

Megalodon
Hom_struct_e_pack

proofgold address
TMWFV..^{Hom_struct_e_pack}

creator
9630 PrCx1../a8c8b..

owner
9630 PrCx1../a8c8b..

term root
266cf..