exact la_nodup.head h.1
case cons.refine_2.refl
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
x : α × β
b : β
a✝ : b ∈ lb
h : a ∈ la ∧ b ∈ lb
⊢ False
no goals