fact: Definition first_index_and_value_option {A} (ls : list (option A)) : option (nat * A) := first_index_helper (B := option (nat * A)) (fun x => match x with | None => false | Some _ => true end) (fun x => match x with | Some (x1, Some x2) => Some (x1, x2) | _ => None end) ls (fun x => x).
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality