右に型更新演算子が含まれるとき

証明ターゲット S ⊆ y<<K を考える。

y<<K は、暗黙に y も y<<K もオブジェクト型であることを含意しているので、Sがオブジェクト型でないときは証明ターゲットは成立しない。したがって、http://d.hatena.ne.jp/m-hiyama-memo/19100110/1263114915 の左側分類で可能性があるのは：

1. Sがオブジェクト型
2. Sが変数
3. Sがジョイン型

Sがジョイン型は分解還元処理により、他の2つの場合に帰着する。Sが変数のとき、証明ターゲットは x ⊆ y<<K 。これは、Kをopen-constraintsで解釈した型を K↑ として、x ⊆ (K↑) となり、今までの（<<なしの）推論に帰着できる。

---

K = {α:U, β:V} とする。まず、

1. S.α⊆ y.α
2. S.β⊆ y.β

はこのまま出力する。他のユニフィケーションとSIL推論によりyは具体化または消去される可能性がある。γをαともβとも違う名前だとして、S.γ⊆y.γ も同様な扱いになる。yが具体化されないままだと、これらの条件は実行時検査条件としては消去される。