diff --git a/unify.tex b/unify.tex index 887e14a..7db53b6 100644 --- a/unify.tex +++ b/unify.tex @@ -774,7 +774,7 @@ This builds a search tree over multiple possible solutions. \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a}\\ \hline \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a}, - \tv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}}, + \ntv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}}, %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards \overline{\tv{u} \lessdot \type{S}} }