proposition: Lemma SN_incl A (S R : rel A) : R << S -> forall x, SN S x -> SN R x.
proof: Proof. intros RS x hx. eapply SN_inclusion. apply RS. refl. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)