exact anyM_loop_cons_succ p a x h start
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
start stop : Nat
h : stop ≤ size x
⊢ anyM.loop p (cons a x) (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (size x)) (start + 1) = anyM.loop p x stop h start
no goals