rewrite [anyM_cons_zero (m:=Id) p a x]
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ anyM p (cons a x) 0 (stop + 1) = (p a || anyM p x 0 stop)
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (do
      let b ← p a
      if b = true then pure true else anyM p x 0 stop) =
    (p a || anyM p x 0 stop)