proposition: Lemma elements_iff_find : forall (elt : Type) (m : t elt) (x : key) (e : elt), find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x, e) (elements (elt:=elt) m).
proof: Proof. intros; rewrite <- elements_iff. rewrite find_mapsto_iff; reflexivity. 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