proposition: Lemma WF_union_mod : WF E -> WF (E# @ R) -> WF (R U E).
proof: Proof. intros WF_E WF_ER x. apply SN_ind with A (E# @ R); auto. clear x. intros x _ IH. apply SN_intro. intros y RExy. destruct RExy as [Rxy | Exy]. apply IH. exists x. split; [apply rt_refl | hyp]. cut (forall y, (E# @ R) x y -> SN (R U E) y); [idtac | hyp]. cut (E! x y). pattern y. apply SN_ind with A E; auto. clear y IH Exy. intros y _ IH_out Exy IH_in. apply SN_intro. intros z REyz. destruct REyz. apply IH_in. exists y. split; trivial. apply tc_incl_rtc. hyp. apply IH_out; trivial. constructor 2 with y. trivial. constructor. hyp. constructor. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)