proposition: Lemma wf_union_Rcdp_rest : well_founded (Rcdp_rest dps_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:=Rcdp_rest dps_large); [ apply dps_large_wf |]; clear t. intros t IH2 IH1; constructor; intros s [H Hrest]; destruct H as [f l1 l2 t Hl1_l2 Ht]; inversion Ht; clear Ht; subst. destruct (dps_union_def _ _ H1). apply IH1; apply rtc_R_step with l2; [| assumption ]; rewrite <- H; apply dps_strictly_decrease; assumption. apply IH2. split; [| assumption ]; split with (l2:=l2); [ assumption |]; rewrite <- H; constructor; assumption. intros x Hx; apply IH1; apply rtc_R_step with l2; [| assumption ]; apply Tlt_Tle_compat with (M.apply_subst sigma t1); [ assumption |]; rewrite <- H; apply dps_large_decrease; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)