proposition: Lemma refine_ListComprehension_Equiv {A} : forall (As : list A) (P Q : A -> Prop), (forall a, P a <-> Q a) -> refine (⟦element in As | P element ⟧) (⟦element in As | Q element ⟧).
proof: Proof. induction As; simpl; intros; eauto. - reflexivity. - rewrite IHAs; eauto. apply refine_bind. reflexivity. intros ? ? ?. computes_to_inv; destruct v0; simpl in *. + apply (@BindComputes _ _ _ _ true); eauto. computes_to_econstructor; simpl; eauto. apply H; assumption. + apply (@BindComputes _ _ _ _ false); eauto. computes_to_econstructor; simpl; intros. intro; apply H0. apply H; eassumption. Qed.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation