proposition: Lemma FullySharpenedBagsEquivMatchers : forall (ElementType SearchTermType UpdateTermType : Type) (MatchSearchTerm MatchSearchTerm' : SearchTermType -> ElementType -> bool) (ApplyUpdateTerm ApplyUpdateTerm' : UpdateTermType -> ElementType -> ElementType), (forall st item, MatchSearchTerm st item = MatchSearchTerm' st item) -> (forall ut item, ApplyUpdateTerm ut item = ApplyUpdateTerm' ut item) -> FullySharpened (BagSpec MatchSearchTerm ApplyUpdateTerm) -> FullySharpened (BagSpec MatchSearchTerm' ApplyUpdateTerm').
proof: Proof. intros; exists (projT1 X). pose (projT2 X); simpl in *. assert (MatchSearchTerm = MatchSearchTerm') as M_eq by (apply functional_extensionality; intros; apply functional_extensionality; eauto); destruct M_eq. assert (ApplyUpdateTerm = ApplyUpdateTerm') as A_eq by (apply functional_extensionality; intros; apply functional_extensionality; eauto); destruct A_eq. exact r. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Arith.Arith Coq.Structures.OrderedTypeEx Fiat.Common.String_as_OT Fiat.Common.i2list Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.ADTRefinement.GeneralBuildADTTactics Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.Common.List.ListFacts TransparentAbstract