Coqリポジトリのtrunkを見ると、次の2つの機能が入っていることがわかります。 Universe Polymorphism Primitive Projection Universe Polymorphismは、グローバル定義をUniverseのレベルについて量化した形で定義することができる機能で、型に飾り付けをし…