proposition: Lemma eqFM_Equiv : equivalence eqFM.
proof: Proof. red in |- *. split; [ try assumption | idtac ]. exact eqFM_refl. red in |- *. split; [ try assumption | idtac ]. exact eqFM_trans. exact eqFM_sym. Qed.
imports: Monoid_cat Sgroup_facts Monoid_facts Monoid_util