intro hik h
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
⊢ i ≤ ↑k → loop p i hi = none → p k = false
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h : loop p i hi = none
⊢ p k = false