diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 9b419f942277093a1c37f3a2271955b7ef8d9f95..10b491f98f41eb9fb7525cd7fa44d2d2fd1f0b86 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -254,7 +254,19 @@ An example of such a transformation is the following:}
     %\cnotv[0.6] \rTo^* 
     \cnotvi[0.7]
   \]~\\[-4mm]%
-Members of our consortium have demonstrated how to use these formal reasoning techniques in software, including the interactive theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which was used to formally verify quantum communication protocols and error correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr}) and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early demonstration of the capacity of the \zxcalculus to \newt{outperform other methods of circuit optimisation,  in the sense that certain circuit metric (such as total size, tree-width, or number of non-Clifford subterms such as T-gates) can be minimised.}
+Members of our consortium have demonstrated how to use these formal
+reasoning techniques in software, including the interactive theorem
+prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which
+was used to formally verify quantum communication protocols and error
+correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr})
+and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early
+demonstration of the capacity of the \zxcalculus to \newt{outperform
+  other methods of circuit optimisation,  in the sense that certain
+  circuit metric (such as total size, tree-width, or number of
+  non-Clifford subterms such as T-gates) can be minimised.}  Our
+industry partner CQC develops \tket, a retargetable quantum compiler
+which, using \zx-based optimisations, outperforms all existing
+compilers for quantum software.
 \TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
 %%% cutting because repeated later
 % It is strictly more powerful than the stabiliser