have goal := nodupkeys_eq_of_fst_eq nd h h' rfl
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
⊢ b = b'
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : (a, b) = (a, b')
⊢ b = b'