proposition: Lemma Vcast_cast_eq : forall n (v : vector A n) m (h1 : n=m) p (h2 : m=p) (h3 : n=p), Vcast (Vcast v h1) h2 = Vcast v h3.
proof: Proof. intros ? ? ? [] ? []; auto using Vcast_refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)