シーケントの多目的使用

1. 関数・定理の定義・記述 Γ |- ψ : A
2. 型推論問題の質問 Γ |-? ψ : ?
3. 項推論問題の質問 Γ |-? ? : A
4. プロファイル宣言 Γ |- _ : A （アンダースコアは不定の意味）
5. 単なる省略 Γ |- ψ : _ （不定だが、型推論で確定可能）
6. ホムセット {f | f: Γ |- _ : A}

毎回、確認しなくてはならない。