rewrite [getElem_eq rfl (dif_neg hstop)]
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : ¬stop ≤ n
⊢ p x[if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start] = true
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : ¬stop ≤ n
⊢ p x[findIdx.loop x p n (_ : Nat.le n n) start] = true