fact: Fixpoint first_index_partial {A} (f : A -> option bool) (ls : list A) : option (option nat) := match ls with | nil => Some None | x :: xs => match f x with | None => None | Some b => if b then Some (Some 0) else match first_index_partial f xs with | Some (Some i) => Some (Some (S i)) | v => v end end end.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality