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
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
⊢ (fun x x_1 => x <$> x_1) f <$> Sum.traverse g x = Sum.traverse ((fun x x_1 => x <$> x_1) f ∘ g) x
cases x <;> simp [Sum.traverse, id_map, functor_norm] <;> congr