proposition: Lemma Vapp_nil : forall n (v : vector A n) (w : vector A 0), Vapp v w = Vcast v (plus_n_O n).
proof: Proof. intros. apply Vapp_nil_eq. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)