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