proposition: Lemma refine_Where' {A B} : forall (P : Ensemble A) (P_dec : DecideableEnsemble P) (bod : Comp (list B)), forall a, refine (if (dec a) then bod else (ret nil)) (Where (P a) bod)%QuerySpec.
proof: Proof. unfold refine, Query_Where; intros. computes_to_inv; intuition. caseEq (dec a). apply dec_decides_P in H; eauto. rewrite H1; eauto. unfold not; intros H'; apply dec_decides_P in H'; congruence. 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