proposition: Lemma Vapp_eq : forall n1 (v1 v1' : vector A n1) n2 (v2 v2' : vector A n2), Vapp v1 v2 = Vapp v1' v2' <-> v1 = v1' /\ v2 = v2'.
proof: Proof. induction v1; simpl. intro. VOtac. simpl. intros. tauto. intro. VSntac v1'. simpl. split; intro. Veqtac. subst h. rewrite IHv1 in H3. intuition. rewrite H0. refl. destruct H0. Veqtac. subst h. apply Vcons_eq_intro. refl. rewrite IHv1. intuition. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)