proposition: Lemma proj_cons_rtc_l : forall t n (v : terms n), red proj_cons # (cons_term t v) t.
proof: Proof. intros. case v. simpl. apply rt_refl. intros t' n' v'. apply rt_step. apply proj_cons_l. Qed.
imports: CoLoR(ATrs VecUtil ListUtil LogicUtil NatUtil RelUtil)