by_cases i = k.val with
| isTrue heq =>
  rw [Bool.eq_false_iff]
  intro hk
  apply hp
  rw [←hk]
  congr
| isFalse hik' =>
  have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
  exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
no goals