proposition: Lemma Vcast_cast : forall n (v : vector A n) m (h1 : n=m) p (h2 : m=p), Vcast (Vcast v h1) h2 = Vcast v (trans_eq h1 h2).
proof: Proof. intros. apply Vcast_cast_eq. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)