proposition: Lemma WF_mod_rev : WF (E# @ S) -> WF (S @ E#).
proof: Proof. intro wf. cut (WF (E# @ S @ E#)). intro wf'. eapply WF_incl. 2: apply wf'. intros x z [y [xy yz]]. exists y. intuition. exists x. intuition. apply absorb_WF_modulo_r. 2: hyp. intros x z [y [xy yz]]. destruct yz as [t [yt tz]]. exists t. intuition. apply rt_trans with y. apply rt_step. hyp. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)