proposition: Lemma absorb_SN_modulo_r : forall x, SN T x -> SN (T @ R#) x.
proof: Proof. induction 1. apply SN_intro. intros. apply SN_intro. intros. do 2 destruct H1. do 2 destruct H2. assert (T x0 x1). apply (absorbs_left_rtc absorb). exists y. intuition. ded (H0 _ H1). eapply SN_inv. 2:apply H6. exists x1. intuition. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)