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