fact: Definition first_index_default {A} (f : A -> bool) (default : nat) (ls : list A) : nat := first_index_helper f (option_rect (fun _ => nat) fst default) ls (fun x => x).
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality