proposition: Theorem ulist_app_inv_l: forall (l1 l2 : list A), ulist (l1 ++ l2) -> ulist l1.
proof: Proof. intros l1; elim l1; simpl; auto. intros a l H l2 H0. inversion H0 as [|il1 iH1 iH2 il2 [iH4 iH5]]; apply ulist_cons; auto. intros H5; case iH2; auto with datatypes. apply H with l2; auto. Qed.
imports: List Arith Permutation ListSet