proposition: Lemma Equal_elements {A} : forall m1 m2, Equal m1 m2 -> forall k (a : A), (InA (@eq_key_elt _) (k, a) (elements m1) <-> InA (@eq_key_elt _) (k, a) (elements m2)).
proof: Proof. unfold Equal; split; intros; rewrite <- elements_mapsto_iff, find_mapsto_iff in H0; rewrite <- elements_mapsto_iff, find_mapsto_iff; congruence. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances