proposition: Lemma proj_cons_tc_r : forall n (v : terms n) t x, Vin x v -> red proj_cons ! (cons_term t v) x.
proof: Proof. intro n. induction v; intros. simpl in H. tauto. apply tc_merge. exists (cons_term h v). split. apply proj_cons_r. destruct H. rewrite H. apply proj_cons_rtc_l. apply tc_incl_rtc. apply IHv; auto. Qed.
imports: CoLoR(ATrs VecUtil ListUtil LogicUtil NatUtil RelUtil)