proposition: Lemma Vcast_pi : forall n (v : vector A n) p (h1 : n=p) (h2 : n=p), Vcast v h1 = Vcast v h2.
proof: Proof. intros; f_equal; apply eq_proofs_unicity. intros x y; case (eq_nat_dec x y); tauto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)