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

State before:
α : Type u_1
a : α
l : List α
⊢ (a :: l).Nodup ↔ ¬a ∈ l ∧ l.Nodup
Tactic:
simp only [Nodup, pairwise_cons, forall_mem_ne]
State after:
no goals