proposition: Lemma sn_restrict : Proper (R ==> impl) P -> forall x, SN (restrict P R) x -> P x -> SN R x.
proof: Proof. intro P_R. induction 1. intro px. apply SN_intro; intros y xy. apply H0. fo. rewrite <- xy. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter) CoLoR(Path) CoLoR(SetUtil)