proposition: Lemma SN_commut_modulo : forall x, SN S x -> SN (R# @ S) x.
proof: Proof. induction 1. apply SN_intro. intros. ded (commut_rtc commut H1). do 2 destruct H2. eapply SN_modulo. apply H0. apply H2. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)