no goals
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
⊢ [] ∈ traverse f [] ↔ Forall₂ (fun b a => b ∈ f a) [] []
simp
no goals
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
a : α'
as : List α'
⊢ [] ∈ traverse f (a :: as) ↔ Forall₂ (fun b a => b ∈ f a) [] (a :: as)
simp
no goals
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f [] ↔ Forall₂ (fun b a => b ∈ f a) (b :: bs) []
simp
no goals
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
α' β' : Type u
f✝ : α' → F β'
inst✝ : LawfulApplicative F
f : α' → Set β'
a : α'
as : List α'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f (a :: as) ↔ Forall₂ (fun b a => b ∈ f a) (b :: bs) (a :: as)
simp [mem_traverse as bs]