proposition: Lemma Vcast_eq_intror : forall n1 (v1 : vector A n1) n0 (h1 : n1=n0) n2 (v2 : vector A n2) (h2 : n2=n0) (h : n1=n2), Vcast v1 h = v2 -> Vcast v1 h1 = Vcast v2 h2.
proof: Proof. intros until h1; case h1; intros; simpl; subst v2. rewrite Vcast_cast, Vcast_refl; refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)