proposition: Lemma refineEquiv_For_DropQSConstraints A qsSchema qs : forall bod, refine {H1 | exists or' : QueryStructure qsSchema * list A, (queryRes <- (For bod)%QuerySpec; ret (qs, queryRes)) ↝ or' /\ DropQSConstraints_AbsR (fst or') (fst H1) /\ snd or' = snd H1} (b <- (For bod)%QuerySpec; ret (DropQSConstraints qs, b) ) .
proof: Proof. setoid_rewrite refineEquiv_pick_ex_computes_to_bind_and; intros; f_equiv; unfold pointwise_relation; intros. setoid_rewrite refineEquiv_pick_ex_computes_to_and; setoid_rewrite refineEquiv_bind_unit; simpl; unfold DropQSConstraints_AbsR; setoid_rewrite refineEquiv_pick_pair; setoid_rewrite refineEquiv_pick_eq'; simplify with monad laws; f_equiv. 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