rw [dif_neg i.not_lt_zero]
case refl
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
i : Nat
⊢ (if hlt : i < 0 then
      let_fun this := (_ : i < size #[]);
      do
      let __do_lift ← p #[][i]
      if __do_lift = true then pure true else anyM.loop p #[] 0 (_ : Nat.le 0 0) (i + 1)
    else pure false) =
    pure false
no goals