proposition: Lemma SN_vred_imp_SN_ared : forall t, SN (vred S) t -> forall u, t = vterm_of_aterm u -> SN (ared R) u.
proof: Proof. induction 1. intros. subst x. apply SN_intro. intros. apply (H0 (vterm_of_aterm y)). apply vred_of_ared. exact H1. refl. Qed.
imports: CoLoR(LogicUtil ListUtil VecUtil SN)