refine Nat.decreasing_induction (m:=0) (n:=as.size) ?_ ?_ as.size.zero_le
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any (List.drop 0 as.data) p
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