proposition: Lemma eqFMd_Equiv : equivalence eqFMd.
proof: Proof. red in |- *. split; [ try assumption | idtac ]. exact eqFMd_refl. red in |- *. split; [ try assumption | idtac ]. exact eqFMd_trans. exact eqFMd_sym. Qed.
imports: Module_util Module_facts