それが逆なんじゃないかなと思って。 P.Protocol が existential P の型じゃない？ ↑のcheckPE経由のcheckTの結果から判断した。 (edited)