proposition: Lemma refine_Iterate_Decided_Ensemble_Pre : forall (Remaining : nat) (P : Ensemble (Fin.t Remaining)) (Q : Prop), refine {b | Q -> decides b (Iterate_Ensemble_BoundedIndex' P)} (Iterate_Decide_Comp_Pre Remaining P Q).
proof: Proof. induction Remaining; simpl; intros. - computes_to_econstructor; computes_to_inv; subst; simpl; auto. - computes_to_econstructor; computes_to_inv; destruct_ex; split_and; computes_to_inv; subst. destruct v0; simpl in *. { destruct v; simpl in *; intuition; intros; eauto. - generalize (IHRemaining _ _ _ H'). intros; computes_to_inv; simpl in *; eauto. - generalize (IHRemaining _ _ _ H'). intros; computes_to_inv; simpl in *; eauto. eapply H; eauto. } { computes_to_inv; subst; simpl; intuition. } 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