proposition: Lemma Vsub_nil_aux : forall i k (h:i+k<=0) (e : 0=k), Vsub Vnil h = Vcast Vnil e.
proof: Proof. destruct k; intros. rewrite Vcast_refl; refl. discr. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)