Misc setoids lemmas and tweaks for maps and option

• Add lemmas map_singleton_equiv_inj and map_fmap_equiv_inj.
• Add lemma option_fmap_equiv_inj.
• Add Propers for maps, and generalize existing ones. Add tests to check that the old ones can be derived.
• Add lemma map_equiv_lookup_r.
• Add lemma map_equiv_iff.

Also, rename instances option_mbind_proper → option_bind_proper and option_mjoin_proper → option_join_proper to be consistent with similar instances for sets and lists.