proposition: Lemma Vcast_refl n (v : vector A n) : forall H : n=n, Vcast v H = v.
proof: Proof. apply K_dec_type; auto with arith. Defined.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)