no goals
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
bs : List α'
⊢ traverse f ([] ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f []) fun x => traverse f bs
simp [functor_norm]
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (Seq.seq
      (Seq.seq (((fun x => x ∘ fun x x_1 => x ++ x_1) ∘ Function.comp ∘ fun x x_1 => x :: x_1) <$> f a) fun x =>
        traverse f as)
      fun x => traverse f bs) =
    Seq.seq (Seq.seq (((fun x => (fun x x_1 => x ++ x_1) ∘ x) ∘ fun x x_1 => x :: x_1) <$> f a) fun x => traverse f as)
      fun x => traverse f bs
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ traverse f (a :: as ++ bs) = Seq.seq ((fun x x_1 => x ++ x_1) <$> traverse f (a :: as)) fun x => traverse f bs
simp [traverse_append as bs, functor_norm]
no goals
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (Seq.seq
      (Seq.seq (((fun x => x ∘ fun x x_1 => x ++ x_1) ∘ Function.comp ∘ fun x x_1 => x :: x_1) <$> f a) fun x =>
        traverse f as)
      fun x => traverse f bs) =
    Seq.seq (Seq.seq (((fun x => (fun x x_1 => x ++ x_1) ∘ x) ∘ fun x x_1 => x :: x_1) <$> f a) fun x => traverse f as)
      fun x => traverse f bs
congr