proposition: Lemma wf_rel_mod : WF (S# @ R) -> WF ((R U S)# @ (R' U S')) -> WF ((S' U S)# @ (R' U R)).
proof: Proof. intros. apply WF_incl with ((S' U S)# @ (R U R')). comp. apply union_commut. apply wf_mod_shift. apply WF_incl with (S# @ (R' U S') U S# @ R). intros x y Q. destruct Q as [z [Sxz [[Rxz | R'xz] | S'xz]]]; solve [ right; exists z; intuition | left; exists z; intuition]. apply WF_union_mod. hyp. apply WF_incl with ((R U S)# @ (R' U S')); [idtac | hyp]. intros x y Q. destruct Q as [z [Lxz [w [Szw RSwy]]]]. exists w. split; [idtac | hyp]. constructor 3 with z. apply incl_rtc_rtc with (S# @ R); [idtac | intuition]. intros a b B. destruct B as [c [Sac Rcb]]. constructor 3 with c; [idtac | intuition]. apply rtc_incl with S; intuition. apply rtc_incl with S; intuition. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter) CoLoR(Path)