proposition: Lemma Vsub_eq_nil k n (v : vector A n) i (h : i+k <= n) (hk : k = 0) : Vsub v h = Vcast Vnil (eq_sym hk).
proof: Proof. subst k. rewrite Vcast_refl; refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)