proposition: Lemma wf_restrict_sn : P [<=] SN R -> WF (restrict P R).
proof: Proof. intros h x. apply SN_intro; intros y [hx xy]. gen (SN_inv xy (h _ hx)). clear x hx xy. revert y; induction 1. apply SN_intro. fo. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter) CoLoR(Path) CoLoR(SetUtil)