さらに用語の整理
言葉と記号法の問題が色々とある。
型代入（type substitution, 行為とオペレータの意味がある）は構文的操作、型環境は意味論的な概念としよう。そう定義する。型環境は型評価に使う。型評価は型計算と言ってもいいが、型項を具体化して結果として具体型を求めること。
型項と名前を関係付けることは割り当て（assignment）、型のlet束縛といってもいい。代入（置換）とは違う。が、代入（置換）、割り当て、束縛はテキトーに使っているな、僕も皆んなも。区別しがたいこともあるし。
型具体化って言葉もあいまいで、具体型による型代入なのか、型環境における型評価かわからない。同値なら同値という証明が必要だ。
「いわゆる型推論」、あるいは僕が「型推論」から連想するような行為は実は不要だったような気がする -- これは前例や既存の知識にこだわり過ぎだった。従来の型推論とかはスッパリ忘れて、非対称単一化の結果を中心にすべきかも。
それと、記号法も不十分； ラムダ式で言えば λ(x∈A, y∈B).E のような形を考えているのだが、これはどうもダメで、λ(x, y:C).E のような形だろう。ここで、Cはx, yを含む（かも知れない）論理式。
「・」をアプライ演算子として、(λ(x, y:C).E)・(a, b) が許されるのは、|- C(a, b) のときに限るとする。こうすると、λ(x∈A, y∈B).E は、λ(x, y : x∈A ∧ y∈B).E の略記となる。|= (a∈A ∧ b∈B) のときに、(a, b)による代入（具体化）ができる。
型ラムダ式にも同じ記法を採用すると、λ
