p.201の真ん中あたりの依存型理論について少々．一つの例をあげると、型INTの整数nに対してそのn次元整数ベクトル（配列）を返す関数vを考えてみる．引数に対応して値域の型がになっているので、vの型はどうしたもんかということになる．Xを型INTとして、Aの…