proposition: Lemma Vcast_eq_elim : forall n (v1 v2 : vector A n) m (h : n = m), Vcast v1 h = Vcast v2 h -> v1 = v2.
proof: Proof. intros until h; case h; trivial. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)