proposition: Lemma proj_cons_l : forall n (v : terms n) t a, red proj_cons (cons_term t (Vcons a v)) t.
proof: Proof. pose (Vxy := (Vcast (Vcons (Var 0) (Vcons (@Var Sig 1) Vnil)) cons_arity)). intros. exists (Fun (Cons Sig) Vxy). exists (Var 0). exists Hole. pose (s := fun i => match i with | 0 => t | S j => match j with | 0 => (cons_term a v) | S k => t end end). exists s. split. unfold proj_cons. rewrite In_cons. left. refl. split. 2: simpl; auto. rewrite cons_term_cons. unfold Vxy. apply args_eq. apply Veq_nth. intros i Hi. rewrite Vnth_map, !Vnth_cast. destruct i. simpl; refl. rewrite !Vnth_cons. destruct i. simpl; refl. cut (S (S i) < 2). intro; lia. rewrite cons_arity; auto. Qed.
imports: CoLoR(ATrs VecUtil ListUtil LogicUtil NatUtil RelUtil)