proposition: Lemma rpo_rpo_eq_compat : Trel_compat (Rpo.rpo P n) (Rpo.rpo_eq P n).
proof: Proof. intros t1 t2 t3 H H0; inversion H0; subst; [ apply (proj1 (@Rpo.equiv_rpo_equiv_1 P _ _ _ H1 _) H) | apply Rpo.rpo_trans with t2; assumption ]. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)