rw [hp, cond_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 : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : p x[i] = true
⊢ (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) = ?m.160149
no goals