proposition: Lemma Vtail_eq : forall a n (v1 v2 : vector A n), v1 = v2 -> Vcons a v1 = Vcons a v2.
proof: Proof. intros. apply Vcons_eq_intro. refl. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)