. 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.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
no goals