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