proposition: Corollary refine_UnConstrQuery_In_Query_Where_Cond {qs_schema} : forall (r_n : UnConstrQueryStructure qs_schema) Ridx (ResultT : Type) (P Q : _ -> Prop) (body : _ -> Comp (list ResultT)), (forall tup, P tup <-> Q tup) -> refine (UnConstrQuery_In r_n Ridx (fun tup => Query_Where (P tup) (body tup))) (UnConstrQuery_In r_n Ridx (fun tup => Query_Where (Q tup) (body tup))).
proof: Proof. intros; apply refine_UnConstrQuery_In; intro. apply refine_Query_Where_Cond; eauto. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Specification.Operations.Empty