proposition: Lemma MValues_elements_in_iff: forall (elt : Type) (m : MValues.t elt) (x : MValues.key), MValues.In x m <-> (In x (map fst (MValues.elements m))).
proof: Proof. unfold MValues.In. setoid_rewrite MoreMValuesFacts.BasicFacts.elements_mapsto_iff. intros; induction (MValues.elements m); split; simpl; intros. - destruct_ex; inversion H. - inversion H. - destruct_ex; inversion H; subst. destruct H1; simpl in *; subst; eauto. right; eapply IHl; eauto. - inversion H; subst. eexists (snd a); constructor; destruct a; split; simpl; eauto. apply IHl in H0; destruct_ex; eexists; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.Peano_dec Coq.Structures.OrdersEx Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListInclusion