proposition: Lemma SN_modulo : forall x x', SN (E# @ R) x -> E# x x' -> SN (E# @ R) x'.
proof: Proof. intros. apply SN_intro. intros. eapply SN_inv. 2: apply H. do 2 destruct H1. exists x0. intuition. apply rt_trans with x'; hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)