fact: Fixpoint dprod A B al (f : A -> list B) := match al with | nil => nil | a :: al => map (fun b => (a, b)) (f a) ++ dprod al f end.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation