no goals
α : Type u_3
β : Type u_2
γ : Type u_1
δ : Type ?u.20275
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → α
x✝ : List β
⊢ Forall₂ R (map f []) x✝ ↔ Forall₂ (fun c b => R (f c) b) [] x✝
simp only [map, forall₂_nil_left_iff]
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
δ : Type ?u.20275
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → α
a : γ
l : List γ
x✝ : List β
⊢ Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b => R (f c) b) (a :: l) x✝
simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]