proposition: Lemma stable_monotone_R_list : inclusion _ (one_step_list (Eqt.one_step R)) (one_step_list O).
proof: Proof. set (P2 := fun t1 t2 => Eqt.one_step R t1 t2 -> O t1 t2); set (Pl2 := fun l1 l2 => one_step_list (Eqt.one_step R) l1 l2 -> one_step_list O l1 l2); change (forall l1 l2, Pl2 l1 l2); apply M.term_rec8 with P2; unfold P2 in *; unfold Pl2 in *; clear P2 Pl2. intros v t H; inversion H; subst; destruct H0; apply R_stable; assumption. intros t v H; inversion H; subst; destruct H0; apply R_stable; assumption. intros f1 f2 l1 l2 H H0; inversion H0; subst; [ destruct H1; apply R_stable; assumption | apply O_monotone; apply H; assumption ]. induction l1; intros l2 H H0; inversion H0; subst; [ constructor 1; apply H; [| | assumption ]; left; reflexivity | constructor 2; apply IHl1; [| assumption ]; intros; apply H; try right; assumption ]. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)