proposition: Corollary refineEquiv_For_Query_Where_And {ResultT} {qs_schema} : forall (r : UnConstrQueryStructure qs_schema) idx P P' bod, (forall tup, P tup \/ ~ P tup) -> refine (For (UnConstrQuery_In r idx (fun tup => @Query_Where ResultT (P tup /\ P' tup) (bod tup)))) (For (UnConstrQuery_In r idx (fun tup => Where (P tup) (Where (P' tup) (bod tup))))).
proof: Proof. intros; apply refine_refine_For_Proper. apply refine_UnConstrQuery_In_Proper. intro; apply refineEquiv_Query_Where_And; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Compose Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Lib2.WordOpt Fiat.Narcissus.Lib2.NatOpt Fiat.Narcissus.Lib2.StringOpt Fiat.Narcissus.Lib2.EnumOpt Fiat.Narcissus.Lib2.FixListOpt Fiat.Narcissus.Lib2.SumTypeOpt Fiat.Common.SumType Fiat.Examples.Tutorial.Tutorial Fiat.Examples.DnsServer.DecomposeEnumField Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.Examples.HACMSDemo.DuplicateFree Fiat.QueryStructure.Automation.MasterPlan Bedrock.Word Bedrock.Memory