proposition: Lemma Vapp_nil_eq : forall n (v : vector A n) (w : vector A 0) (h : n=n+0), Vapp v w = Vcast v h.
proof: Proof. induction v; intros. VOtac; rewrite Vcast_refl; refl. rewrite (Vcast_cons h0), <- (IHv w); refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)