proposition: Lemma SN_same_ext A (R S : rel A) : R == S -> forall x, SN R x <-> SN S x.
proof: Proof. intros RS x. split; intro hx. apply (SN_incl R); fo. apply (SN_incl S); fo. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)