proposition: Lemma SN_tc : forall x, SN R x -> SN (R!) x.
proof: Proof. induction 1. apply SN_intro. intros. ded (tc_split H1). do 2 destruct H2. apply SN_inv_rtc with (x := x0). apply incl_elim with (R := R#). apply rtc_incl. apply incl_tc. refl. hyp. apply H0. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)