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