proposition: Theorem ulist_map: forall (A B : Set) (f : A -> B) l, (forall x y, (In x l) -> (In y l) -> f x = f y -> x = y) -> ulist l -> ulist (map f l).
proof: Proof. intros a b f l Hf Hl; generalize Hf; elim Hl; clear Hf; auto. simpl; auto. intros a1 l1 H1 H2 H3 Hf; simpl. apply ulist_cons; auto with datatypes. contradict H1. case in_map_inv with ( 1 := H1 ); auto with datatypes. intros b1 [Hb1 Hb2]. replace a1 with b1; auto with datatypes. Qed.
imports: List Arith Permutation ListSet