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