reflexivity, stub of wrapping theorems

paper/gtt.tex

@@ -721,6 +721,18 @@ While we have shown
 
 \subsection{Uniqueness Principles for Casts}
 
+Now we turn to our main theorem, that the wrapping implementations of
+contracts are the unique implementations that satisfy the $\eta$
+principles of each type, given in figure TODO ref.
+%
+
+\begin{figure}
+  \begin{mathpar}
+    TODO
+  \end{mathpar}
+  \caption{Uniqueness Principles for Casts}
+\end{figure}
+
 \section{Contract Translation to Call-by-push-value}
 
 \subsection{Call-by-push-value operational semantics}
@@ -1164,6 +1176,9 @@ relation from the pole.
     S_2[\unroll \bullet]$ and $M \logpole M'$.
   \end{enumerate}
 \end{proof}
+\begin{corollary}[Reflexivity/Monotonicity]
+  For any $\Gamma \vdash M : \u B$, $\Gamma \vdash M \logpole M \in \u B$
+\end{corollary}
 
 \begin{theorem}[Completeness of Logical wrt Contextual]
   For any pole $\pole$, the logical lifting is complete with respect