no goals
σ✝ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
σ α : Type u_1
x : σ ⊕ α
⊢ Sum.traverse pure x = x
cases x <;> rfl