exact get_findIdx_loop x p stop h' start h
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
h : findIdx.loop x p stop hstop start < stop
⊢ p x[findIdx.loop x p stop hstop start] = true
no goals