cosmetic changes, began proofs: hom_uniq, hom_impl_map