cases h
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
stop : Nat
h : stop ≤ 0
i : Nat
⊢ anyM.loop p #[] stop h i = pure false
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ anyM.loop p #[] 0 (_ : Nat.le 0 0) i = pure false