fact: Fixpoint first_index_recr {A B R} (f : A -> B -> option R) (ls : list A) (ls' : list B) : option (nat * R) := match ls, ls' with | nil, _ => None | _, nil => None | x::xs, y::ys => match f x y with | None => option_map (fun ab => (S (fst ab), snd ab)) (first_index_recr f xs ys) | Some r => Some (0, r) end end.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality