exact congrArg Prod.snd
case cons.refine_1.hf
α : Type u
β : Type v
lb : List β
lb_nodup : Nodup lb
a : α
la : List α
la_nodup : Nodup (a :: la)
IH : Nodup (List.product la lb)
b₁ b₂ : β
⊢ (a, b₁) = (a, b₂) → b₁ = b₂
no goals