rewrite [getElem_eq rfl (dif_pos hi)]
α : 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
hi : i < stop
h :
  (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) <
    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
α : 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
hi : i < stop
h :
  (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) <
    stop
⊢ p
      x[let_fun this := (_ : i < n);
        bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] =
    true