α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ Disjoint l₁ l₂
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ l₁ ∩ l₂ = [] ↔ Disjoint l₁ l₂
simp only [eq_nil_iff_forall_not_mem, mem_inter, not_and]
no goals
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ Disjoint l₁ l₂
rfl