α✝ : Type u_1
l l₁ l₂ : List α✝
⊢ Disjoint l₁ l ∧ Disjoint l₂ l ↔ Disjoint l l₁ ∧ Disjoint l l₂
α✝ : Type u_1
l l₁ l₂ : List α✝
⊢ Disjoint (l₁ ++ l₂) l ↔ Disjoint l l₁ ∧ Disjoint l l₂
rw [disjoint_append_left]
no goals
α✝ : Type u_1
l l₁ l₂ : List α✝
⊢ Disjoint l₁ l ∧ Disjoint l₂ l ↔ Disjoint l l₁ ∧ Disjoint l l₂
simp [disjoint_comm]