exact congr_arg _ (funext $ Fin.cases rfl (fun i => rfl))
case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (pure fun i => cases (v 0) (fun i => v i.succ) i) = pure v
no goals