. induction l with
  | nil => exact False.elim $ List.not_mem_nil s h
  | cons hd tl ih =>
    rw [List.Nodupkeys, List.Nodup, List.Pairwise_iff] at nd
    simp only [List.map_eq_nil, ne_eq] at nd
    rcases nd with l_eq_nil | ⟨a, l', nd⟩
    . exact False.elim l_eq_nil
    . rw [List.Nodupkeys, List.Nodup] at ih
      rcases nd with ⟨nd1, nd2, nd3⟩
      rw [List.map_cons] at nd3
      simp only [List.cons.injEq] at nd3
      rcases nd3 with ⟨hd_fst_eq_a, nd3⟩
      rw [← nd3] at nd2
      specialize ih nd2
      rw [List.mem_cons] at h h'
      rcases h with s_eq_hd | s_in_tl
      . rcases h' with s'_eq_hd | s'_in_tl
        . rw [s_eq_hd, s'_eq_hd]
        . rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
          specialize nd1 s'.1
          simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
            forall_exists_index] at nd1
          specialize nd1 s'.2 s'_in_tl
          exfalso
          exact nd1 keys_eq
      . rcases h' with s'_eq_hd | s'_in_tl
        . rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
          specialize nd1 s.1
          simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
            forall_exists_index] at nd1
          specialize nd1 s.2 s_in_tl
          exfalso
          exact nd1 keys_eq.symm
        . exact ih s_in_tl s'_in_tl
case right
α : 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.snd = s'.snd
no goals