added wrap, proved: wrap_inj, unproved: hom_uniq, hom_map, fst_hom