proposition: Lemma refine_filtered_list : forall (xs : list A) (P : Ensemble A) (P_dec : DecideableEnsemble P), refine (build_FilteredList xs P) (ret (filter dec xs)).
proof: Proof. unfold build_FilteredList; induction xs; intros. - reflexivity. - simpl; setoid_rewrite IHxs. simplify with monad laws. destruct (dec a) eqn: eq_dec_a; [ setoid_rewrite dec_decides_P in eq_dec_a; refine pick val true | setoid_rewrite Decides_false in eq_dec_a; refine pick val false ]; auto; simplify with monad laws; reflexivity. Qed.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation