have goal_rw : (s = s') = (s.1 = s'.1 ∧ s.2 = s'.2) := by
  have s_rw : s = (s.1, s.2) := rfl
  have s'_rw : s' = (s'.1, s'.2) := rfl
  rw [s_rw, s'_rw]
  simp only [Prod.mk.injEq]
α : 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'
α : 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
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s = s'