unfold findIdx.loop at h ⊢
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
h : findIdx.loop x p stop hstop i < stop
x✝ : findIdx.loop x p stop hstop i < n
⊢ p x[findIdx.loop x p stop hstop i] = true
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
h :
  (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
    else stop) <
    stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true