左に型更新演算子が含まれるとき
xは変数、Kは変数を含まない型マップ、Tは任意の型（型項、型表現）だとして、証明ターゲット x<<K ⊆ T を考える。
x<<K は、暗黙に x も x<<K もオブジェクト型（明示的タグもなく、確定（非オプショナル）型）であることを含意しているので、Tがオブジェクト型でないときは証明ターゲット x<<K ⊆ T は成立しない。
したがって、http://d.hatena.ne.jp/m-hiyama-memo/19100110/1263114915 の右側分類で可能性があるのは：
- Tがオブジェクト型
- Tがオプショナル型
- Tが排他的ユニオン型
- Tがインターセクション型
- Tが変数
このなかで、オプショナル型、排他的ユニオン型、インターセクション型は分解還元処理を続けると、Tがオブジェクト型または変数のケースに帰着できる。Tが変数yのときは、証明ターゲットは x<<K ⊆ y で、推論は終り。
残るは、Tがオブジェクト型のとき。
話を簡単にするために、K = {α:U, β:V} とする。まず、
- x.α⊆T.α
- x.β⊆T.β
だが、これは
- U⊆T.α
- V⊆T.β
Tはオブジェクト型なので、T.α、T.βはwell-defined、UとVも決まった型だから、U⊆T.α, V⊆T.β は新しい証明ターゲットとなり、従来と同様な推論を継続（進行）できる。
γをαともβとも違う名前だとして、x.γ⊆T.γ は、T.γ がわかっても、これ以上はどうにもならない。ユニフィケーションの出力としては、α、β以外のすべてのγに対する x.γ⊆T.γ を出力する。Tに型変数が含まれるときは、T内の型が他のユニフィケーションの効果により具体化される可能性がある。最終的に残った (_.γ)∈T.γ をすべて実行時検査条件に加えるしかない。
