proposition: Theorem ulist_list_prod: forall (A : Set) (l1 l2 : list A), ulist l1 -> ulist l2 -> ulist (list_prod l1 l2).
proof: Proof. intros A l1 l2 Hl1 Hl2; elim Hl1; simpl; auto. intros a l H1 H2 H3; apply ulist_app; auto. apply ulist_map; auto. intros x y _ _ H; inversion H; auto. intros p Hp1 Hp2; case H1. case in_map_inv with ( 1 := Hp1 ); intros a1 [Ha1 Ha2]; auto. case in_list_prod_inv with ( 1 := Hp2 ); intros b1 [c1 [Hb1 [Hb2 Hb3]]]; auto. replace a with b1; auto. rewrite Ha2 in Hb1; injection Hb1; auto. Qed.
imports: List Arith Permutation ListSet