case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = tail✝
⊢ (Seq.seq (cons head✝) fun x => tail✝) = head✝ :: tail✝
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
xs : List α
⊢ List.traverse pure xs = xs
induction xs <;> simp! [*, List.traverse, functor_norm]
no goals
case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse pure tail✝ = tail✝
⊢ (Seq.seq (cons head✝) fun x => tail✝) = head✝ :: tail✝
rfl