diff --git a/ITP/symmetry-breaking.tex b/ITP/symmetry-breaking.tex
index c7496e4..bec445c 100644
--- a/ITP/symmetry-breaking.tex
+++ b/ITP/symmetry-breaking.tex
@@ -11,7 +11,7 @@
 there exists a list of points in \emph{canonical position} with the same triple-orientations.
 Canonical position is defined as follows.
 \begin{definition}[Canonical Position]
-A list of points~$L = (p_1,\ldots, p_{n})$ is said to be in \emph{canonical position} if it satisfies all the following properties:
+A list of points~$L = (p_1,\ldots, p_{n})$ is said to be in \emph{canonical position} if it satisfies all of the following properties:
 \begin{itemize}
     \item \textbf{(General Position)} No three points are collinear, i.e., for all $1 \leq i < j < k \leq n$, we have $\sigma(p_i, p_j, p_k) \neq 0$.
     \item \textbf{($x$-order)} The points are sorted with respect to their $x$-coordinates, i.e., $x(p_i) < x(p_j)$ for all $1 \leq i < j \leq n$.
diff --git a/ITP/triple-orientations.tex b/ITP/triple-orientations.tex
index bb0aa0d..00c3f38 100644
--- a/ITP/triple-orientations.tex
+++ b/ITP/triple-orientations.tex
@@ -2,7 +2,7 @@
 problems concerning the existence of an object~$\mathcal{O}$ in a continuous search space like $\mathbb{R}^2$
 must be reformulated in terms of the existence of a discrete, finitely-representable object~$\mathcal{O}'$
 that a computer can search for.
-It is especially challenging to discretize problems in which the desired geometric object $\mathcal{O}$ is characterized by very specific coordinates of points,
+It is especially challenging to discretize problems for which the desired geometric object~$\mathcal{O}$ is characterized by very specific coordinates of points,
 thus requiring the computer to use floating-point arithmetic,
 which suffers from numerical instability.
 Fortunately,
@@ -177,7 +177,7 @@
 
 
 % Let us now discuss the previous steps. First,~\lstinline|(PtInTriangle a p q r)| presents a \emph{ground-truth}  definition for membership in a triangle, in terms of~\textsf{mathlib}'s \lstinline|ConvexHull| definition,  whereas~\lstinline|(σPtInTriangle a p q r)| is based on orientations.
-Heule and Scheucher used the orientation-based definition~\cite{emptyHexagonNumber}, and as it is common in the area, its equivalence to the \emph{ground-truth} mathematical definition was left implicit.
+Heule and Scheucher used the orientation-based definition~\cite{emptyHexagonNumber}, and, as is common in the area, its equivalence to the \emph{ground-truth} mathematical definition was left implicit.
 This equivalence, formalized in~\lstinline|theorem σPtInTriangle_iff| is not trivial to prove:
 the forward direction in particular requires reasoning about convex combinations and determinants.
 Using the previous theorem, we can generalize to $k$-gons as follows.
@@ -214,7 +214,7 @@
 SAT encodings for Erd\H{o}s-Szekeres-type problems use triple orientations to capture properties like convexity and emptiness,
 thus discretizing the problem.
 Because we have proved that $\pi_k(S)$ is an orientation property,
-the values of $\sigma$ on the points in $S$ contain enough information to determine whether $\pi_k(S)$.
+the values of $\sigma$ on the points in $S$ contain enough information to determine whether $\pi_k(S)$ holds.
 Therefore, we have proved that given $n$ points,
 it is enough to analyze the values of $\sigma$ over these points,
 a discrete space with at most $2^{n^3}$ possibilities,