proposition: Lemma Vcons_eq_elim : forall a1 a2 n (v1 v2 : vector A n), Vcons a1 v1 = Vcons a2 v2 -> a1 = a2 /\ v1 = v2.
proof: Proof. intros. Veqtac. auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)