proposition: Lemma SN_modulo_r : forall x x', SN (T @ R#) x -> R# x x' -> SN (T @ R#) x'.
proof: Proof. intros. apply SN_intro. intros. eapply SN_inv. 2: apply H. do 2 destruct H1. ex x0. split_all. apply (absorbs_left_rtc absorb). ex x'. split_all. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)