proposition: Lemma Vcast_lr : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) (h12 : n1=n2) (h21 : n2=n1), Vcast v1 h12 = v2 -> v1 = Vcast v2 h21.
proof: Proof. intros; subst v2; rewrite Vcast_cast, Vcast_refl; refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)