Theorem: Misc.List.nodup_append (LeanSAT/Util/Misc.lean)

State before:
α : Type u_1
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂
Tactic:
simp only [Nodup, pairwise_append, disjoint_iff_ne]
State after:
no goals