proposition: Lemma Vbreak_eq_app_cast : forall n n1 n2 (H : n1+n2=n) (v : vector A n), v = Vcast (Vapp (fst (Vbreak (Vcast v (sym_equal H)))) (snd (Vbreak (Vcast v (sym_equal H))))) H.
proof: Proof. intros until H; case H; simpl; intro v. rewrite <- Vbreak_eq_app; refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)