. intro x
  let ⟨_,b⟩ := x
  simp only [mem_map, Prod.mk.injEq, exists_eq_right_right, and_imp, pair_mem_product]
  intro _ ha h; cases ha
  exact la_nodup.head h.1
case cons.refine_2
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ ∀ (a_1 : α × β), a_1 ∈ List.map (Prod.mk a) lb → ¬a_1 ∈ List.product la lb
no goals