exact findIdx_loop_le x p stop h (i+1)
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif false then i else findIdx.loop x p stop h (i + 1)) ≤ stop
no goals