proposition: Lemma Vsub_app_l : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) (h : 0+n1<=n1+n2), Vsub (Vapp v1 v2) h = v1.
proof: Proof. induction v1; simpl; intros. refl. apply Vtail_eq. rewrite Vsub_cons, IHv1. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)