diff --git a/paper-new/intro.tex b/paper-new/intro.tex
index c0ca56cfd46e46edec857af6eca2a103d27bce7e..d5f1b03eab1ce0bb344c89893c4eef28ecabe3b3 100644
--- a/paper-new/intro.tex
+++ b/paper-new/intro.tex
@@ -2,16 +2,16 @@
   
 % gradual typing, graduality
 \subsection{Gradual Typing and Graduality}
-One of the principal categories on which type systems of programming languages are classified
-is that of static versus dynamic type discipline.
-In static typing, the code is type-checked at compile time, while in a dynamic typing,
+One of the principal ways of categorizing type systems of programming languages is
+whether they are \emph{static} or \emph{dynamic}.
+In static typing, the code is type-checked at compile time, while in dynamic typing,
 the type checking is deferred to run-time. Both approaches have benefits: with static typing,
 the programmer is assured that if the program passes the type-checker, their program
 is free of type errors. Meanwhile, dynamic typing allows the programmer to rapidly prototype
 their application code without needing to commit to fixed type signatures for their functions.
 
-\emph{Gradually-typed languages} \cite{siek-taha06} allow for both disciplines
-to be used in the same codebase, and support interoperability between statically-typed
+\emph{Gradually-typed languages} \cite{siek-taha06} allow for both static and dynamic typing disciplines
+to be used in the same codebase, and support smooth interoperability between statically-typed
 and dynamically-typed code.
 This flexibility allows programmers to begin their projects in a dynamic style and
 enjoy the benefits of dynamic typing related to rapid prototyping and easy modification
@@ -53,9 +53,9 @@ These allow the language developer to start with a statically typed langauge and
 gradually typed language that satisfies the gradual guarantee. The downside to these approaches
 is that the semantics of the resulting languages are too lazy: the frameworks consider only
 the $\beta$ rules and not the $\eta$ equalities. Furthermore, while these frameworks do prove
-graduality, they do not show the correctness of the equational theory, which is equally important
-to sound gradual typing. For example, programmers often refactor their code without thinking about
-whether the refactoring has broken the semantics of the program. 
+graduality of the resulting languages, they do not show the correctness of the equational theory,
+which is equally important to sound gradual typing. For example, programmers often refactor their
+code without thinking about whether the refactoring has broken the semantics of the program. 
 It is the validity of the laws in the equational theory that guarantees that such refactorings are sound. 
 Similarly, correctness of compiler optimizations rests on the validity of the corresponding equations
 from the equational theory. It is therefore important that the langages that claim to be gradually typed
@@ -101,7 +101,7 @@ gradually-typed languages with nontrivial features.
 
 
 \subsection{Proving Graduality in SGDT}
-\textbf{TODO:} This section should probably be moved to after the relevant background has been introduced.
+\textbf{TODO:} This section should probably be moved to after the relevant background has been introduced?
 
 % TODO introduce the idea of cast calculus and explicit casts?
 
diff --git a/paper-new/paper.pdf b/paper-new/paper.pdf
index 8da106e491b64786eb6649373af63f726b36f28f..c86537d615c0a4764a703e1d8b1c9c23e7bf844d 100644
Binary files a/paper-new/paper.pdf and b/paper-new/paper.pdf differ
diff --git a/paper-new/syntax.tex b/paper-new/syntax.tex
index d4d156ec31ff4254699010d06be420c89b40fdd3..96f0bf83e33b44492c5789238dbddca6b05ff9a2 100644
--- a/paper-new/syntax.tex
+++ b/paper-new/syntax.tex
@@ -375,7 +375,7 @@ that it is the \emph{greatest} lower bound.
 % depend on the specific constructs of the language.
 
 
-\subsection{Removing Transitivity}
+\subsection{Removing Transitivity as a Primitive}
 
 The first observation we make is that transitivity of type precision, and heterogeneous
 transitivity of term precision, are admissible. That is, consider a related language which
@@ -409,7 +409,7 @@ More specifically, consider the following situation in $\extlc$:
   
 
 
-\subsection{Removing Casts}
+\subsection{Removing Casts as Primitives}
 
 % We now observe that all casts, except those between $\nat$ and $\dyn$
 % and between $\dyn \ra \dyn$ and $\dyn$, are admissible, in the sense that