proposition: Lemma SN_compat_inv : forall x, SN (R @ E) x -> forall x', E x x' -> SN (R @ E) x'.
proof: Proof. intros. apply SN_intro. intros. do 2 destruct H1. assert (h : (R @ E) x y). exists x0; split. apply (incl_elim Hcomp). exists x'; split; hyp. hyp. eapply SN_inv. apply h. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)