proposition: Lemma rpo_lex_same_length : forall l l', rpo_lex l l' -> length l = length l'.
proof: Proof. induction l; intros l' rpo_lex_l; inversion rpo_lex_l. simpl; rewrite H3; trivial. simpl; rewrite (IHl l'0); trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term