proposition: Lemma SN_red_ren : forall t : term, SN (red R) t -> SN (red R) (sub s t).
proof: Proof. induction 1. apply SN_intro. intros. destruct (red_ren H1). destruct H2. subst. apply H0. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)