. unfold anyM.loop; dsimp
  rewrite [dif_neg (Nat.lt_irrefl _), List.drop_eq_nil_of_le .refl]
  rfl
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
no goals