proposition: Lemma wf_mod_shift : WF (T# @ (R U S)) -> WF ((S U T)# @ R).
proof: Proof. intro. apply WF_incl with ((T # @ (R U S)) !). intros x y Rxy. apply tc_split_inv. apply comp_assoc. destruct Rxy as [z [STxz Rzy]]. exists z. split; [idtac | intuition]. apply rtc_union. apply rtc_incl with (S U T); trivial. intros s t STst. destruct STst as [Sst | Tst]; solve [intuition]. apply WF_tc. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter) CoLoR(Path)