proposition: Lemma bfind_matcher_eq (heading : RawHeading) {BagType SearchTermType UpdateTermType : Type} (TBag : Bag BagType (@RawTuple heading) SearchTermType UpdateTermType) projection : NatRangeTreeBag.RangeTreeBag_bfind_matcher TBag projection = @bfind_matcher _ _ _ _ (NatRangeTreeBag' _ _ projection bupdate_transform).
proof: Proof. repeat (apply functional_extensionality; intros). destruct x as [ [ [st | ] [st' | ] ] st'']; unfold NatRangeTreeBag.RangeTreeBag_bfind_matcher, NatRangeTreeBag.Range_InRange; simpl; unfold NatRangeTreeBag.X_le_dec; simpl; unfold InRange_dec; repeat first [ solve [ eauto ] | match goal with | |- context[Nat_as_OT.compare ?st ?st'] => destruct (Nat_as_OT.compare st st'); simpl | |- context[le_dec ?st ?st'] => destruct (le_dec st st'); simpl end | progress (unfold Nat_as_OT.lt, Nat_as_OT.eq in *; omega) ]. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.Structures.OrderedTypeEx Fiat.Common.String_as_OT Fiat.QueryStructure.Implementation.DataStructures.Bags.RangeTreeBags Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.SearchTerms.InRange Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples 