dsimp [anyM]
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
⊢ anyM p (cons a x) (start + 1) (stop + 1) = anyM p x start stop
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h (start + 1)
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) (start + 1)) =
    if h : stop ≤ size x then anyM.loop p x stop h start else anyM.loop p x (size x) (_ : size x ≤ size x) start