proposition: Lemma arrow_cast : forall n (Ts : Tys n) U n' (h:n=n'), arrow (Vcast Ts h) U = arrow Ts U.
proof: Proof. induction Ts; intros U n' e; subst; rewrite Vcast_refl; refl. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)