proposition: Theorem olist_ulist: forall l, olist l -> ulist l.
proof: Proof. intros l; elim l; simpl; auto. intros a l1; case l1; auto. intros b l2 Rec H; inversion_clear H as [| H0 H1 |]. apply ulist_cons; auto. simpl; intros [H2 | H2]; subst; auto. rewrite weight_refl in H0; discriminate. generalize (weight_anti_sym a b); rewrite H0. rewrite olist_weight with (l := l2); auto. intros; discriminate. Qed.
imports: List Permutation UList