specialize IH la_nodup.tail
case cons
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
IH : Nodup la → Nodup (List.product la lb)
la_nodup : Nodup (a :: la)
⊢ 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.product (a :: la) lb)