rewrite [dif_neg hlt, List.drop_eq_nil_of_le (Nat.le_of_not_lt hlt)]
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : ¬j < size as
⊢ Id.run
      (if hlt : j < size as then
        if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)
      else false) =
    List.any (List.drop j as.data) p
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
hlt : ¬j < size as
⊢ Id.run false = List.any [] p