proposition: Lemma In_mergeSearchTerm_MatchCombineSearchTerm {SearchTermT1 SearchTermT2 : Type} : forall Pattern (a : CombineSearchTerm SearchTermT1 SearchTermT2) (st : list _), List.In Pattern (merge_SearchTerm a st) -> exists st' : SearchTermT2, List.In st' st /\ Pattern = (fst a, Some st') /\ snd a = None.
proof: Proof. intros. destruct a as [a [ ? | ] ]; simpl in *; intuition. rewrite in_map_iff in H; destruct_ex; intuition subst; eauto. Qed.
imports: Coq.Lists.List Coq.Program.Program Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.ilist3 Fiat.Common.i3list Fiat.Common.Ensembles.IndexedEnsembles Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.Common.ilist3_pair Fiat.Common.ilist3 Fiat.Common.i3list2 Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagImplementation