proposition: Lemma Vsub_id : forall n (v : vector A n) (h:0+n<=n), Vsub v h = v.
proof: Proof. induction v; simpl; intros. refl. apply Vtail_eq. rewrite Vsub_cons, IHv. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)