rewrite [dif_pos hlt, ← List.get_drop_eq_drop _ _ hlt, List.any_cons, List.getElem_eq_get, ← Array.getElem_eq_data_get]
α : 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 (if p as[j] = true then true else anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) =
    (p as[j] || List.any (List.drop (j + 1) as.data) p)