conv =>
  arg 1
  dsimp [List.product, List.bind]
  change lb.map (Prod.mk a) ++ la.product lb
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.product (a :: la) lb)
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
⊢ Nodup (List.map (Prod.mk a) lb ++ List.product la lb)