From 1a3cf1c78e69ef7314a0333734c767f90109fb35 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Thu, 8 Feb 2024 14:53:40 +0100
Subject: [PATCH] Change equals

---
 unify.tex | 62 +++++++++++++++++++++++++++----------------------------
 1 file changed, 31 insertions(+), 31 deletions(-)

diff --git a/unify.tex b/unify.tex
index fb94092..8c1e316 100644
--- a/unify.tex
+++ b/unify.tex
@@ -253,37 +253,37 @@ $
     \end{array} \quad \text{fv}(\type{U}, \type{L}) \subseteq \Delta_in
     $
     \\\\
-\rulename{Equals} %TODO
-    & $
-    \begin{array}[c]{l}
-        \wildcardEnv \vdash C \cup \, \set{ \type{N} \doteq \type{N'} } \\ 
-        \hline
-        \vspace*{-0.4cm}\\
-        \wildcardEnv \vdash C \cup \, 
-        \set{
-           \type{N} \lessdot \type{N'}, \type{N'} \lessdot \type{N}
-        }
-    \end{array} % \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset 
-    $
-    \\\\
-    %  \rulename{Equals} %TODO
-    % & $
-    % \begin{array}[c]{l}
-    %     \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\ 
-    %     \hline
-    %     \vspace*{-0.4cm}\\
-    %     \wildcardEnv \vdash C \cup \, 
-    %     \set{
-    %       %  \pi(\ol{T}) \doteq  \pi(\ol{T'} )
-    %       \ol{T} \doteq \ol{T'}
-    %     }
-    % \end{array}
-% \quad \begin{array}{l}
-% \text{given a permutation}\ \pi\ \text{with:}\\
-% \pi(\Delta) = \pi(\Delta')
-% \end{array}
-%    $
-%    \\\\
+% \rulename{Equals} %TODO
+%     & $
+%     \begin{array}[c]{l}
+%         \wildcardEnv \vdash C \cup \, \set{ \type{N} \doteq \type{N'} } \\ 
+%         \hline
+%         \vspace*{-0.4cm}\\
+%         \wildcardEnv \vdash C \cup \, 
+%         \set{
+%            \type{N} \lessdot \type{N'}, \type{N'} \lessdot \type{N}
+%         }
+%     \end{array} % \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset 
+%     $
+%      \\\\
+ \rulename{Equals} %TODO
+& $
+\begin{array}[c]{l}
+    \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\ 
+    \hline
+    \vspace*{-0.4cm}\\
+    \wildcardEnv \vdash C \cup \, 
+    \set{
+      \pi(\ol{T}) \doteq  \pi(\ol{T'} )
+      %\ol{T} \doteq \ol{T'}
+    }
+\end{array}
+\quad \begin{array}{l}
+\text{given a permutation}\ \pi\ \text{with:}\\
+\pi(\Delta) = \pi(\Delta')
+\end{array}
+   $
+   \\\\
     \rulename{Erase}
     & $
     \begin{array}[c]{l}