proposition: Theorem lexico_exact: forall a b, lexico a b = eq -> a = b.
proof: Proof. intros a; elim a; simpl; auto; clear a. intros b; case b; auto. intros; discriminate. intros x a Rec b; case b; auto; clear b. intros; discriminate. intros y b. generalize (weight_exact x y). case (weight x y); auto. intros; discriminate. intros; f_equal; auto. intros; discriminate. Qed.
imports: List Permutation UList