∀ {α : Type u_1} {l : List α} {p : α → Bool} (_x : (xs : List α) ×' (i : ℕ) ×' xs.length + i = l.length),
  List.findIdx?.go p _x.1 _x.2.1 = Option.map (fun x => ↑x) (List.findFinIdx?.go p l _x.1 _x.2.1 ⋯)