intro keys_eq
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
⊢ s.fst = s'.fst → s = s'
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
⊢ s = s'