>>76
http://researchmap.jp/mu1x9nhhd-21099/?action=multidatabase_action_main_filedownload&;download_flag=1&upload_id=40760&metadata_id=12105
> 定義 2.13 型理論の言語 L^T は以下の要素を持つ
　・・・
> * 任意の項τに対し、ある n が存在して項σが type n であり、項τが type n+1 を持つ時
> 　のみ論理式 σ∈τ は有意味な論理式となる。

x∪{x} = {y | y∈x or y∈{x}}
変数ｙのtypeは何になるかね？