proposition: Lemma stable_monotone_R_term : inclusion _ (Eqt.one_step R) O.
proof: Proof. intros t1 t2 H; inversion H; subst; [ inversion H0; subst; apply R_stable | apply O_monotone; apply stable_monotone_R_list ]; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)