proposition: Theorem ulist_app: forall l1 l2, ulist l1 -> ulist l2 -> (forall (a : A), In a l1 -> In a l2 -> False) -> ulist (l1 ++ l2).
proof: Proof. intros L1; elim L1; simpl; auto. intros a l H l2 H0 H1 H2; apply NoDup_cons; simpl; auto. red; intros H3; case in_app_or with ( 1 := H3 ); auto; intros H4. inversion H0; auto. apply H2 with a; auto. apply H; auto. apply ulist_inv with ( 1 := H0 ); auto. intros a0 H3 H4; apply (H2 a0); auto. Qed.
imports: List Arith Permutation ListSet