proposition: Lemma rtc_red_ren : forall t u, red R # (sub s t) u -> exists v, red R # t v /\ sub s v = u.
proof: Proof. cut (forall t' u, red R # t' u -> forall t, t' = sub s t -> exists v, red R # t v /\ sub s v = u). intros. apply H with (t':=sub s t). hyp. refl. induction 1; intros; subst. destruct (red_ren H). exists x. intuition. exists t. intuition. destruct (IHclos_refl_trans1 t (eq_refl (sub s t))). destruct H1. symmetry in H2. destruct (IHclos_refl_trans2 x H2). exists x0. split_all. apply rtc_trans with x; hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)