diff --git a/unify.tex b/unify.tex index c648428..797d2a7 100644 --- a/unify.tex +++ b/unify.tex @@ -370,16 +370,16 @@ Their upper and lower bounds are fresh type variables. \begin{array}[c]{@{}ll} \begin{array}[c]{l} \wildcardEnv \vdash C \cup \, \set{ - \tv{a} \lessdot \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot \wctype{\Delta'}{D'}{\ol{T'}} }\\ + \tv{a} \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}} }\\ \hline \vspace*{-0.4cm}\\ \wildcardEnv \vdash C \cup \, \left\{ \begin{array}[c]{l} \tv{a} \lessdot \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}, \ol{\tv{l}} \lessdot \ol{\tv{u}}, \\ \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}} - \lessdot \wctype{\Delta}{D}{\ol{T}}, \\ + \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \\ \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}} - \lessdot \wctype{\Delta'}{D'}{\ol{T'}} + \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}} \end{array} \right\} \end{array}