proposition: Lemma EquivSearchTerm_App {heading : RawHeading} {SearchTermT' : SearchUpdateTerms heading} {P : Ensemble (@RawTuple heading)} {Patterns1 Patterns2} (eqv_Patterns1 : EquivSearchTerm SearchTermT' P Patterns1) (eqv_Patterns2 : EquivSearchTerm SearchTermT' P Patterns2) : EquivSearchTerm SearchTermT' P (Patterns1 ++ Patterns2).
proof: Proof. econstructor; intros. apply in_app_or in H; intuition. eauto using (OK_search_pattern eqv_Patterns1). eauto using OK_search_pattern. 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