rw [pure_bind]
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : ¬i < size x
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)
no goals