case refl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h h' : { fst := a, snd := b } ∈ l
⊢ b = b
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
a : α
b b' : β a
l : List (Sigma β)
nd : NodupKeys l
h : { fst := a, snd := b } ∈ l
h' : { fst := a, snd := b' } ∈ l
⊢ b = b'
cases nd.eq_of_fst_eq h h' rfl
no goals
case refl
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
a : α
b : β a
l : List (Sigma β)
nd : NodupKeys l
h h' : { fst := a, snd := b } ∈ l
⊢ b = b
rfl