proposition: Lemma Vcast_elimlr : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) (h12 : n1=n2), Vcast v1 h12 = v2 -> v1 = Vcast v2 (sym_eq h12).
proof: Proof. intros. eapply Vcast_lr. apply H. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)