proposition: Lemma Vbreak_eq_app : forall n1 n2 (v : vector A (n1+n2)), v = Vapp (fst (Vbreak v)) (snd (Vbreak v)).
proof: Proof. intros n1 n2. elim n1. auto. clear n1. intros n1 Hrec. simpl. intro v. gen (Hrec (Vtail v)); intro H. rewrite VSn_eq at 1. rewrite H at 1. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)