proposition: Lemma refine_Iterate_Ensemble_filter {n} : forall (P : Ensemble (Fin.t n)) (filter : Ensemble (Fin.t n)) (filter_dec : DecideableEnsemble filter), refine {b | decides b (forall idx : _, filter idx -> P idx)} {b | decides b (@Iterate_Ensemble_BoundedIndex_filter n P (@dec _ _ filter_dec) )}.
proof: Proof. intros; eapply refine_pick_pick. intros; destruct x; simpl in *. intros; eapply Iterate_Ensemble_equiv_filter'; eauto using string_dec. destruct n; simpl in *; intros; intuition. unfold not; intros; apply H. case_eq (dec Fin.F1); try econstructor. eapply H0; eapply dec_decides_P; eauto. let f := constr:(@Iterate_Ensemble_equiv_filter'' _ (fun n' : Fin.t n => P (Fin.FS n')) (fun n' : Fin.t n => filter (Fin.FS n')) ({| dec := (fun n' : Fin.t n => dec (Fin.FS n')); dec_decides_P := (fun a => dec_decides_P (Fin.FS a))|})) in eapply f; eauto. intros; let f := constr:(@Iterate_Ensemble_equiv_filter'' _ (fun n' : Fin.t n => P (Fin.FS n')) (fun n' : Fin.t n => filter (Fin.FS n')) ({| dec := (fun n' : Fin.t n => dec (Fin.FS n')); dec_decides_P := (fun a => dec_decides_P (Fin.FS a))|})) in eapply f; eauto. Qed.
imports: Coq.Lists.List Coq.Arith.Compare_dec Coq.Arith.Arith Coq.Bool.Bool Coq.Strings.String Coq.Sets.Ensembles Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.Common.IterateBoundedIndex Fiat.Common.List.ListFacts Fiat.Common.LogicFacts Fiat.Common.DecideableEnsembles Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.ApplyMonad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.General Fiat.Computation.Refinements.Tactics