specialize nd1 s'.1
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : 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 (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ map (fun x => x.fst) tl → ¬s.fst = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : 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 (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : s'.fst ∈ map (fun x => x.fst) tl → ¬s.fst = s'.fst
⊢ s.snd = s'.snd