proposition: Lemma rpo_trans : forall s t u, rpo t s -> rpo u t -> rpo u s.
proof: Proof. intros s t u lt_t_s lt_u_t; elim (rpo_closure s t u); intuition. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term