intro j IH
case refine_1
α : Type u
as : Array α
p : α → Bool
⊢ ∀ (n : Nat),
    Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (n + 1)) = List.any (List.drop (n + 1) as.data) p →
      Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) n) = List.any (List.drop n as.data) p
case refine_1
α : 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
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) j) = List.any (List.drop j as.data) p