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
α : 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 : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
no goals