proposition: Lemma wf_union_R : well_founded (Eqt.one_step R_union).
proof: Proof. intros t; apply well_founded_ind with (R:=Tlt); [ apply Tlt_wf |]; clear t. intros t; pattern t; apply well_founded_ind with (R:=Eqt.one_step R_large); [ apply rules_large_wf |]; clear t. intros t H H0; constructor; intros s Hst. assert (Eqt.one_step R_rules s t \/ Eqt.one_step R_large s t). revert Hst; clear H H0; revert s t; set (P2 := fun s t => Eqt.one_step R_union s t -> Eqt.one_step R_rules s t \/ Eqt.one_step R_large s t); change (forall t1 t2, P2 t1 t2); apply M.term_rec7 with (Pl2 := fun l1 l2 => one_step_list (Eqt.one_step R_union) l1 l2 -> one_step_list (Eqt.one_step R_rules) l1 l2 \/ one_step_list (Eqt.one_step R_large) l1 l2); unfold P2 in *; clear P2. intros v t H; inversion H; subst; inversion H0; subst; rewrite H1; inversion H0; subst; apply rules_union_def in H5; destruct H5; [ left | right ]; constructor; constructor; assumption. intros t v H; inversion H; subst; inversion H0; subst; rewrite H1; inversion H0; subst; apply rules_union_def in H5; destruct H5; [ left | right ]; constructor; constructor; assumption. intros f1 f2 l1 l2 H H0; inversion H0; subst; [ inversion H1; subst; apply rules_union_def in H4; destruct H4; [ left | right ]; constructor; constructor; assumption | apply H in H2; destruct H2; [ left | right ]; apply Eqt.in_context; assumption ]. induction l1; intros l2 H H0; inversion H0; subst. apply H in H4; try (left; reflexivity); destruct H4; [ left | right ]; constructor; assumption. apply IHl1 in H4; [ destruct H4; [ left | right ] | intros; apply H ]; try right; assumption. destruct H1. apply H0; apply stable_monotone_R_term with R_rules; assumption. apply H in H1; [ assumption |]; intros; apply H0; apply Tlt_Tle_compat with s; [ assumption |]; apply stable_monotone_R_term with R_large; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)