diff --git a/paper/gtt.tex b/paper/gtt.tex
index 9efa093cac625342c56aed0b11998fcfeea9ad2f..a83e33cfccb6afe6cb7616b6de666d5e14307e2e 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -9,7 +9,6 @@
 %% For 
 \iflong\documentclass[acmsmall,nonacm]{acmart}\fi
 
-
 %% Note: Authors migrating a paper from PACMPL format to traditional
 %% SIGPLAN proceedings format should change 'acmlarge' to
 %% 'sigplan,10pt'.
@@ -1733,11 +1732,21 @@ our design choice is forced for all casts, as long as the casts between ground t
       \Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
     {\Phi \vdash (V_1,V_2) \ltdyn (V_1',V_2') : A_1 \times A_2 \ltdyn A_1' \times A_2'}
     \quad
+    \inferrule*[lab=$\to$ICong]
+    {\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
+    {\Phi \pipe \Psi \vdash \lambda x : A . M \ltdyn \lambda x' : A' . M' : A \to \u B \ltdyn A' \to \u B'}
+    
+    \\\\
     \inferrule*[lab=$\times$ECong]
     {\Phi \vdash V \ltdyn V' : A_1 \times A_2 \ltdyn A_1' \times A_2' \\\\
       \Phi, x \ltdyn x' : A_1 \ltdyn A_1', y \ltdyn y' : A_2 \ltdyn A_2' \mid \Psi \vdash E \ltdyn E'  : T \ltdyn T'
     }
     {\Phi \mid \Psi \vdash \pmpairWtoXYinZ V x y E \ltdyn \pmpairWtoXYinZ {V'} {x'} {y'} {E'} : T \ltdyn T'}
+    \,\,
+    \inferrule*[lab=$\to$ECong]
+    {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
+      \Phi \vdash V \ltdyn V' : A \ltdyn A'}
+    {\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
     \\\\
 \iflong
     \inferrule*[lab=$U$ICong]
@@ -1758,15 +1767,6 @@ our design choice is forced for all casts, as long as the casts between ground t
       \Phi, x \ltdyn x' : A \ltdyn A' \pipe \cdot \vdash N \ltdyn N' : \u B \ltdyn \u B'} 
     {\Phi \pipe \Psi \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x'} {N'} : \u B \ltdyn \u B'} 
     \\\\
-    \inferrule*[lab=$\to$ICong]
-    {\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
-    {\Phi \pipe \Psi \vdash \lambda x : A . M \ltdyn \lambda x' : A' . M' : A \to \u B \ltdyn A' \to \u B'}
-    \qquad
-    \inferrule*[lab=$\to$ECong]
-    {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
-      \Phi \vdash V \ltdyn V' : A \ltdyn A'}
-    {\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
-    \\\\
 \iflong
     \inferrule*[lab=$\top$ICong]{ }{\Phi \mid \Psi \vdash \{\} \ltdyn \{\} : \top \ltdyn \top}
     \qquad
@@ -1787,7 +1787,7 @@ our design choice is forced for all casts, as long as the casts between ground t
   \]
   \vspace{-0.25in}
   \caption{GTT Term Dynamism (Structural and Congruence Rules) \ifshort
-    (Rules for $U,1,+,0,\times,\top$ in extended version)
+    (Rules for $U,1,+,0,\with,\top$ in extended version)
     \fi}
   \label{fig:gtt-term-dynamism-structural}
 \end{small}
@@ -3659,9 +3659,10 @@ Theorems~\ref{thm:functorial-casts} and
                           & & & \bindXtoYinZ{(\force{(f)}\,x)}{y}\\ & & & {\ret{(\upcast{A_2}{A_2'}{y})}})\\
     \end{array}
     \\
-    \begin{array}{l}
-    \dncast{\u F U(A_1 \to \u F A_2)}{\u F U(A_1' \to \u F A_2')}{\bullet} \equidyn 
-    \bindXtoYinZ{\bullet}{f}{\ret{\lambda{x}.{\dncast{\u F A_2}{\u F A_2'}{(\force{(f)} \, (\upcast{A_1}{A_1'}{x}))}}}}
+    \begin{array}{rcl}
+    \dncast{\u F U(A_1 \to \u F A_2)}{\u F U(A_1' \to \u F A_2')}{\bullet} & \equidyn &
+    \bindXtoYinZ{\bullet}{f}\\
+    & & {\ret{\lambda{x}.{\dncast{\u F A_2}{\u F A_2'}{(\force{(f)} \, (\upcast{A_1}{A_1'}{x}))}}}}
     \end{array}
   \end{array}
   \end{small}
@@ -7912,8 +7913,8 @@ The standard progress-and-preservation properties allow us to define
   observe that each of the cases above is preserved by $\step$.
 \end{longproof}
 \begin{definition}[Results]
-   The set of possible results of a computation is $\{ \diverge, \err,
-   \ret \tru, \ret \fls \}$. We denote a result by $R$, and define a
+   The possible results of a computation are $ \diverge, \err,
+   \ret \tru$ and $\ret \fls$. We denote a result by $R$, and define a
    function $\result$ which takes a program $\cdot \vdash M : \u F 2$,
    and returns its end-behavior, i.e., $\result(M)= \diverge$ if $M
    \Uparrow$ and otherwise $M \Downarrow \result(M)$.
@@ -9339,11 +9340,11 @@ $\errordivergerightop$ gives
 Because logical equivalence implies contextual equivalence, we can
 then conclude with the main theorem:
 \begin{theorem}[Contextual Approximation/Equivalence Model CBPV] ~~\\
-  $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ implies
-  $\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T$
-  and 
-  ${\Gamma \pipe \Delta \vdash E \equidyn E' : T}$ implies
-  ${\Gamma \pipe \Delta \vDash E \ctxize= E' \in T}$
+  If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then
+  $\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T$;
+  if
+  ${\Gamma \pipe \Delta \vdash E \equidyn E' : T}$ then
+  ${\Gamma \pipe \Delta \vDash E \ctxize= E' \in T}$.
 \end{theorem}
 \begin{longproof}