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
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
      (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
no goals