proposition: Lemma Vcast_eq : forall n (v1 v2 : vector A n) p (e : n=p), Vcast v1 e = Vcast v2 e <-> v1 = v2.
proof: Proof. split; intro. apply (Vcast_eq_elim H). apply Vcast_eq_intro. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)