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