if hi : i < stop then
  rewrite [dif_pos hi] at h
  rewrite [getElem_eq rfl (dif_pos hi)]
  dsimp at *
  if hp : p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi hstop)) = true then
    rewrite [getElem_eq rfl (by rw [hp, cond_true])]
    exact hp
  else
    have hp := Bool.eq_false_iff.mpr hp
    rewrite [getElem_eq rfl (by rw [hp, cond_false])]
    rewrite [hp, cond_false] at h
    exact get_findIdx_loop x p stop hstop (i+1) h
else
  rewrite [dif_neg hi] at h
  exact absurd h stop.lt_irrefl
α : 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
no goals