fact: Definition first_index_default_partial {A} (f : A -> option bool) (default : nat) (ls : list A) := match first_index_partial f ls with | None => None | Some None => Some default | Some v => v end.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality