proposition: Lemma Vsub_pi : forall n (v : vector A n) i k (h h' : i+k<=n), Vsub v h = Vsub v h'.
proof: Proof. intros. assert (h = h'). apply le_unique. subst. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)