proposition: Lemma elements_in_iff' : forall (elt : Type) (m : t elt) x, In x m <-> exists v, InA (eq_key (elt:=elt)) (x, v) (elements m) .
proof: Proof. split; rewrite elements_in_iff; intros. destruct H; induction H. destruct H; eexists x0; econstructor; eauto. destruct IHInA; econstructor; econstructor 2; eassumption. destruct H; induction H. eexists; repeat econstructor; simpl; eauto. destruct IHInA; eexists; econstructor 2; eauto. 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