no goals
ι : Type ?u.480230
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
l✝ : List α
x : α
l : List α
⊢ All₂ p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1
rw [forall_mem_cons, all₂_cons, all₂_iff_forall]