dsimp [anyM]
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
⊢ anyM p #[] start stop = pure false
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
start stop : Nat
⊢ (if h : stop ≤ 0 then anyM.loop p #[] stop h start else anyM.loop p #[] 0 (_ : size #[] ≤ size #[]) start) =
    pure false