proposition: Lemma SN_tc1 : forall x, SN R x -> SN (R!1) x.
proof: Proof. intros x snx. induction snx as [x IH0 IH1]. apply SN_intro. intros y xRty. destruct xRty. apply IH1. hyp. assert (SNy := IH1 y H). destruct SNy as [SNy]. apply SNy. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)