proposition: Lemma Vbreak_app : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2), Vbreak (Vapp v1 v2) = (v1, v2).
proof: Proof. induction n1; simpl; intros. VOtac. refl. VSntac v1. simpl. gen (IHn1 (Vtail v1) n2 v2). intro. rewrite H0. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)