proposition: Lemma InA_eq_key_eq_key_elt : forall k t l, InA (MValues.eq_key (elt:=TItem)) (k, t) l <-> exists v, InA (@MValues.eq_key_elt _) (k, v) l.
proof: Proof. induction l; simpl; split; intros. - inversion H. - destruct_ex; inversion H. - inversion H; subst. + exists (snd a); destruct a; econstructor; simpl in *. split; simpl; eauto. + rewrite IHl in H1; destruct_ex; eexists; econstructor 2; eauto. - destruct_ex; inversion H; subst. + constructor; apply H1. + econstructor 2; apply IHl; 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