rw [pure_bind]
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ pure (cons b r) = do
    let y ← pure r
    pure (cons b y)
no goals