. intro j IH
  unfold anyM.loop; dsimp
  if hlt : j < as.size then
    rewrite [dif_pos hlt, ← List.get_drop_eq_drop _ _ hlt, List.any_cons, List.getElem_eq_get, ← Array.getElem_eq_data_get]
    if hpj : p (as[j]'hlt) = true then
      rewrite [if_pos hpj, hpj, Bool.true_or]
      rfl
    else
      rw [if_neg hpj, IH, Bool.eq_false_iff.mpr hpj, Bool.false_or]
  else
    rewrite [dif_neg hlt, List.drop_eq_nil_of_le (Nat.le_of_not_lt hlt)]
    rfl
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_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (size as)) = List.any (List.drop (size as) as.data) p
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (size as)) = List.any (List.drop (size as) as.data) p