Proofgold Proposition

MetaFunctor struct_e PtdSetHom (λ x0 . lam_id (ap x0 0)) (λ x0 x1 x2 . lam_comp (ap x0 0)) PtdPred UnaryPredHom (λ x0 . lam_id (ap x0 0)) (λ x0 x1 x2 . lam_comp (ap x0 0)) (λ x0 . unpack_e_i x0 (λ x1 x2 . pack_p x1 (λ x3 . x3 = x2))) (λ x0 x1 x2 . x2)

type
prop

theory
HotG

name
-

proof
PUg5x..

Megalodon
MetaFunctor_struct_e_struct_p_nonempty

proofgold address
TMdyw..^{MetaFunctor_struct_e_struct_p_nonempty}

creator
11300 PrEBh../65f0d..

owner
11305 PrEBh../a7e25..

term root
f195f..