Theorem: List.nodupKeys_cons (Lean4Lean/Std/NodupKeys.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
a : α✝ × β✝
l : List (α✝ × β✝)
⊢ NodupKeys (a :: l) ↔ (∀ (a' : α✝ × β✝), a' ∈ l → a.fst ≠ a'.fst) ∧ NodupKeys l
Tactic:
simp [nodupKeys_iff_pairwise]
State after:
no goals