fact: Fixpoint Iterate_Decide_Comp_opt_Pre (Remaining : nat) (P : Fin.t Remaining -> option Prop) (Q : Prop) {struct Remaining } : Comp bool := match Remaining return (Fin.t Remaining -> option Prop) -> Comp bool with | 0 => fun P => ret true | S Remaining' => fun P => match P Fin.F1 with | Some P' => b' <- {b' | Q -> decides b' P'}; If_Then_Else b' (Iterate_Decide_Comp_opt_Pre Remaining' (fun n => P (Fin.FS n)) Q) (ret false) | None => (Iterate_Decide_Comp_opt_Pre Remaining' (fun n => P (Fin.FS n)) Q) end end%comp P.
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