proposition: Lemma wf_rel_mod_simpl : WF (S# @ R) -> WF ((R U S)# @ R') -> WF (S# @ (R' U R)).
proof: Proof. intros. apply WF_incl with ((empty_rel U S)# @ (R' U R)). comp. apply rtc_incl. intuition. apply wf_rel_mod. hyp. apply WF_incl with ((R U S)# @ R'); trivial. comp. apply union_empty_r. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter) CoLoR(Path)