2016-12-16 型クラス Mizar 課題 型クラス相当機能は分かったが、 型クラスのインスタンス化の方法が分からない。 インスタンス化に証明が伴うが、書き方が分からない。is を使って、X is C と書いて、この命題を証明するのか?