proposition: Lemma refine_Iterate_Ensemble {n} : forall (P : Ensemble (Fin.t n)), refine {b | decides b (forall idx : Fin.t n, P idx)} {b | decides b (@Iterate_Ensemble_BoundedIndex n P)}.
proof: Proof. intros; eapply refine_pick_pick. intros; destruct x; simpl in *. intros; eapply Iterate_Ensemble_equiv'; eauto using string_dec. destruct n; simpl in *; intros; intuition. apply H1; eauto. apply Iterate_Ensemble_equiv''; auto using string_dec. 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