correct impl of function upcast I think

gcbpv.tex

@@ -579,6 +579,7 @@ We implement the appropriate casts and their adjoints as follows
 \[ \upcast {U \u M} {U \dync} x = \u \roll \thunk [ \pi_{\u M} \mapsto \force x; \pi_{\u M'} \mapsto \err ] \]
 
 \begin{figure}
+  \begin{mathpar}
   \inferrule
   {A \vtype \and \u B \ctype}
   {A \to \u B \ctype}
@@ -604,22 +605,25 @@ We implement the appropriate casts and their adjoints as follows
   {\Phi \pipe \Psi \vdash M_1 \ltdyn M_2 : A_1 \to \u B_1 \ltdyn A_2 \to \u B_2 \and
     \Phi \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2}
   {\Phi \pipe \Psi \vdash M_1(v_1) \ltdyn M_2(v_2) : \u B_1 \ltdyn \u B_2}
+  \end{mathpar}
   \caption{Function Type}
 \end{figure}
 
 \begin{figure}
+  \begin{mathpar}
   \inferrule
   {}
-  {\dncast {A_1 \to \u B_1}{A_2 \to \u B_2} \bullet \equidyn \lambda x:A_1. \dncast {\u B_1}{\u B_2} (\bullet(\upcast {A_1} {A_2}))}
+  {\dncast {A_1 \to \u B_1}{A_2 \to \u B_2} \bullet \equidyn \lambda x:A_1. \dncast {\u B_1}{\u B_2} (\bullet(\upcast {A_1} {A_2} x))}
 
   \inferrule
   {}
-  {\upcast {U({A_1 \to \u B_1})}{U({A_2 \to \u B_2})} (f : U(A_1 \to \u B_1)) \equidyn
-    \thunk \lambda x_2 : A_2. \force \upcast{U \u B_1}{U \u B_2}(\thunk ((\force f)))
+  {\upcast {U({A_1 \to \u B_1})}{U({A_2 \to \u B_2})} (f : U(A_1 \to \u B_1)) \equidyn\\
+    \thunk \lambda x_2 : A_2.
+    \lett x_1 = \dncast{\u F A_1}{\u F A_2}\ret x_2;
+    (\force \upcast{U \u B_1}{U \u B_2}(\thunk ((\force f)(x_1))))
   }
-
-  
-  
+    
+  \end{mathpar}
   \caption{Function Contract Theorem, Proof}
 \end{figure}