proposition: Lemma proj_cons_fun : forall f v1 v2, (forall i (Hi : i < arity f), red proj_cons # (Vnth v1 Hi) (Vnth v2 Hi)) -> red proj_cons # (Fun f v1) (Fun f v2).
proof: Proof. intros. gen (proj_cons_fun_aux2 f (Nat.add_0_r (arity f)) Vnil v1 v2 H). rewrite !Vapp_nil, !Vcast_cast, !Vcast_refl; auto. Qed.
imports: CoLoR(ATrs VecUtil ListUtil LogicUtil NatUtil RelUtil)