take four

new_system_beppe.tex

@@ -286,12 +286,16 @@ completeness is more difficult since first we have to prove that if we
 did not find an annotation, then there does not exist an annotation
 that make that term typeable and second that if that particular normal
 form is not typeable then there cannot be any other normal form that
-is typeable and whose erasure it the source language expression.
+is typeable and whose erasure it the source language expression. And
+in any case completeness cannot hold in general since I think it is
+not decidable.
 
 
 \newpage
 
-\section{TAKE FOUR}
+
+{\color{lightgray}
+      \section{TAKE FOUR (OLD VERSION)}
 \subsection{Declarative system}
 
 
@@ -663,3 +667,4 @@ plus context rules to implement an leftmost outermost weak reduction semantics.
     }
     { }
 \end{mathpar}
+}