diff --git a/paper/_minted/12ADCD03C9A93E8738E3EF4CAE987AEF.highlight.minted b/paper/_minted/12ADCD03C9A93E8738E3EF4CAE987AEF.highlight.minted
deleted file mode 100644
index 397f957c4..000000000
--- a/paper/_minted/12ADCD03C9A93E8738E3EF4CAE987AEF.highlight.minted
+++ /dev/null
@@ -1,13 +0,0 @@
-\begin{MintedVerbatim}[commandchars=\\\{\}]
-\PYG{k+kd}{@[}\PYG{n}{equational\PYGZus{}result}\PYG{k+kd}{]}\PYG{+w}{ }\PYG{k+kn}{theorem}\PYG{+w}{ }\PYG{n}{Equation999\PYGZus{}implies\PYGZus{}Equation86}
-\PYG{+w}{    }\PYG{o}{(}\PYG{n}{G}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{k+kt}{Type}\PYG{n+nb+bp}{*}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{[}\PYG{n}{Magma}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{]}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{Equation999}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{Equation86}\PYG{+w}{ }\PYG{n}{G}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{k}{by}
-\PYG{+w}{  }\PYG{n}{by\PYGZus{}contra}\PYG{+w}{ }\PYG{n}{nh}
-\PYG{+w}{  }\PYG{n}{simp}\PYG{+w}{ }\PYG{n}{only}\PYG{+w}{ }\PYG{o}{[}\PYG{n}{not\PYGZus{}forall}\PYG{o}{]}\PYG{+w}{ }\PYG{k}{at}\PYG{+w}{ }\PYG{n}{nh}
-\PYG{+w}{  }\PYG{k}{obtain}\PYG{+w}{ }\PYG{n+nb+bp}{⟨}\PYG{n}{sK0}\PYG{o}{,}\PYG{+w}{ }\PYG{n}{sK1}\PYG{o}{,}\PYG{+w}{ }\PYG{n}{sK2}\PYG{o}{,}\PYG{+w}{ }\PYG{n}{nh}\PYG{n+nb+bp}{⟩}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{nh}
-\PYG{+w}{  }\PYG{k}{have}\PYG{+w}{ }\PYG{n}{eq9}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{X0}\PYG{+w}{ }\PYG{n}{X1}\PYG{+w}{ }\PYG{n}{X2}\PYG{+w}{ }\PYG{n}{X3}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{X1}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{o}{(}\PYG{o}{(}\PYG{n}{X2}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{n}{X3}\PYG{o}{)}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{X1}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{n}{X0}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{n+nb+bp}{=}\PYG{+w}{ }\PYG{n}{X0}\PYG{+w}{ }\PYG{o}{:=}
-\PYG{+w}{    }\PYG{n}{mod\PYGZus{}symm}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{n+nb+bp}{..}\PYG{o}{)}
-\PYG{+w}{  }\PYG{k}{have}\PYG{+w}{ }\PYG{n}{eq10}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{sK0}\PYG{+w}{ }\PYG{n+nb+bp}{≠}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{sK1}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{sK2}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{sK1}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{n}{sK0}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{mod\PYGZus{}symm}\PYG{+w}{ }\PYG{n}{nh}
-\PYG{+w}{  }\PYG{k}{have}\PYG{+w}{ }\PYG{n}{eq11}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{X3}\PYG{+w}{ }\PYG{n}{X4}\PYG{+w}{ }\PYG{n}{X5}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{X4}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{X3}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{X4}\PYG{+w}{ }\PYG{n+nb+bp}{◇}\PYG{+w}{ }\PYG{n}{X5}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{n+nb+bp}{=}\PYG{+w}{ }\PYG{n}{X5}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{superpose}\PYG{+w}{ }\PYG{n}{eq9}\PYG{+w}{ }\PYG{n}{eq9}
-\PYG{+w}{  }\PYG{k}{have}\PYG{+w}{ }\PYG{n}{eq21}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{sK0}\PYG{+w}{ }\PYG{n+nb+bp}{≠}\PYG{+w}{ }\PYG{n}{sK0}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{superpose}\PYG{+w}{ }\PYG{n}{eq11}\PYG{+w}{ }\PYG{n}{eq10}
-\PYG{+w}{  }\PYG{n}{subsumption}\PYG{+w}{ }\PYG{n}{eq21}\PYG{+w}{ }\PYG{n}{rfl}
-\end{MintedVerbatim}
diff --git a/paper/_minted/1FC85BECB7EF9A894AC6562535195B40.highlight.minted b/paper/_minted/1FC85BECB7EF9A894AC6562535195B40.highlight.minted
deleted file mode 100644
index ef549b2c2..000000000
--- a/paper/_minted/1FC85BECB7EF9A894AC6562535195B40.highlight.minted
+++ /dev/null
@@ -1,12 +0,0 @@
-\begin{MintedVerbatim}[commandchars=\\\{\}]
-\PYG{k+kd}{@[}\PYG{n}{equational\PYGZus{}result}\PYG{k+kd}{]}
-\PYG{k+kn}{theorem}\PYG{+w}{ }\PYG{n+nb+bp}{\PYGZus{}}\PYG{n}{root\PYGZus{}}\PYG{n+nb+bp}{.}\PYG{n}{Equation1437\PYGZus{}not\PYGZus{}implies\PYGZus{}Equation4269}\PYG{+w}{ }\PYG{o}{:}
-\PYG{+w}{    }\PYG{n+nb+bp}{∃}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{G}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{k+kt}{Type}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n+nb+bp}{\PYGZus{}}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{Magma}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{)}\PYG{o}{,}\PYG{+w}{ }\PYG{n}{Equation1437}\PYG{+w}{ }\PYG{n}{G}\PYG{+w}{ }\PYG{n+nb+bp}{∧}\PYG{+w}{ }\PYG{n+nb+bp}{¬}\PYG{+w}{ }\PYG{n}{Equation4269}\PYG{+w}{ }\PYG{n}{G}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{k}{by}
-\PYG{+w}{  }\PYG{n}{use}\PYG{+w}{ }\PYG{n}{ℕ}\PYG{+w}{ }\PYG{n+nb+bp}{×}\PYG{+w}{ }\PYG{n}{Fin}\PYG{+w}{ }\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{+w}{ }\PYG{n+nb+bp}{⟨}\PYG{n}{op}\PYG{n+nb+bp}{⟩}
-\PYG{+w}{  }\PYG{n}{constructor}
-\PYG{+w}{  }\PYG{n+nb+bp}{⬝}\PYG{+w}{ }\PYG{n}{intro}\PYG{+w}{ }\PYG{n}{x}\PYG{+w}{ }\PYG{n}{y}\PYG{+w}{ }\PYG{n}{z}
-\PYG{+w}{    }\PYG{n}{simp}\PYG{+w}{ }\PYG{o}{[}\PYG{n}{op}\PYG{o}{,}\PYG{+w}{ }\PYG{n}{add\PYGZus{}assoc}\PYG{o}{]}
-\PYG{+w}{  }\PYG{n+nb+bp}{⬝}\PYG{+w}{ }\PYG{n}{simp}\PYG{+w}{ }\PYG{n}{only}\PYG{+w}{ }\PYG{o}{[}\PYG{n}{not\PYGZus{}forall}\PYG{o}{,}\PYG{+w}{ }\PYG{n}{op}\PYG{o}{]}
-\PYG{+w}{    }\PYG{n}{use}\PYG{+w}{ }\PYG{o}{(}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{0}\PYG{o}{)}\PYG{o}{,}\PYG{+w}{ }\PYG{o}{(}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{0}\PYG{o}{)}
-\PYG{+w}{    }\PYG{n}{decide}
-\end{MintedVerbatim}
diff --git a/paper/_minted/336A906F6F62E71684EE6F94801D4C64.highlight.minted b/paper/_minted/336A906F6F62E71684EE6F94801D4C64.highlight.minted
deleted file mode 100644
index 4115a75c9..000000000
--- a/paper/_minted/336A906F6F62E71684EE6F94801D4C64.highlight.minted
+++ /dev/null
@@ -1,10 +0,0 @@
-\begin{MintedVerbatim}[commandchars=\\\{\},codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax}]
-\PYG{k+kd}{@[}\PYG{n}{equational\PYGZus{}result}\PYG{k+kd}{]}
-\PYG{k+kd}{theorem}\PYG{+w}{ }\PYG{esc}{\textnormal{\guillemotleft}}\PYG{n}{Facts}\PYG{+w}{ }\PYG{k}{from}\PYG{+w}{ }\PYG{n}{All4x4Tables}\PYG{+w}{ }\PYG{o}{[}\PYG{o}{[}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{]}\PYG{o}{,}\PYG{o}{[}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{]}\PYG{o}{,}\PYG{o}{[}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{]}\PYG{o}{,}
-\PYG{o}{[}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{]}\PYG{o}{,}\PYG{o}{[}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{]}\PYG{o}{,}\PYG{o}{[}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{]}\PYG{o}{]}\PYG{esc}{\textnormal{\guillemotright}}\PYG{+w}{ }\PYG{o}{:}
-\PYG{+w}{  }\PYG{n+nb+bp}{∃}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{G}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{k+kt}{Type}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{\PYGZus{}}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{Magma}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{\PYGZus{}}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{Finite}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{)}\PYG{o}{,}\PYG{+w}{ }\PYG{n}{Facts}\PYG{+w}{ }\PYG{n}{G}\PYG{+w}{ }\PYG{o}{[}\PYG{l+m+mi}{1316}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2863}\PYG{o}{]}\PYG{+w}{ }\PYG{o}{[}\PYG{l+m+mi}{411}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{680}\PYG{o}{,}
-\PYG{+w}{  }\PYG{l+m+mi}{817}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{1020}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{1426}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2035}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2441}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2644}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2853}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2855}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2865}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2872}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{2947}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{3050}\PYG{o}{,}
-\PYG{+w}{  }\PYG{l+m+mi}{3253}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{3456}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{4270}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{4283}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{4290}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{4380}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{4598}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{4605}\PYG{o}{,}\PYG{+w}{ }\PYG{l+m+mi}{4656}\PYG{o}{]}\PYG{+w}{ }\PYG{o}{:=}
-\PYG{o}{⟨}\PYG{n}{Fin}\PYG{+w}{ }\PYG{l+m+mi}{6}\PYG{o}{,}\PYG{+w}{ }\PYG{esc}{\textnormal{\guillemotleft}}\PYG{n}{All4x4Tables}\PYG{+w}{ }\PYG{o}{[}\PYG{o}{[}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{]}\PYG{o}{,}\PYG{o}{[}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{]}\PYG{o}{,}\PYG{o}{[}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{]}\PYG{o}{,}\PYG{o}{[}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{]}\PYG{o}{,}
-\PYG{o}{[}\PYG{l+m+mi}{5}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{2}\PYG{o}{]}\PYG{o}{,}\PYG{o}{[}\PYG{l+m+mi}{2}\PYG{o}{,}\PYG{l+m+mi}{3}\PYG{o}{,}\PYG{l+m+mi}{0}\PYG{o}{,}\PYG{l+m+mi}{1}\PYG{o}{,}\PYG{l+m+mi}{4}\PYG{o}{,}\PYG{l+m+mi}{5}\PYG{o}{]}\PYG{o}{]}\PYG{esc}{\textnormal{\guillemotright}}\PYG{o}{,}\PYG{+w}{ }\PYG{n}{Finite.of\PYGZus{}fintype}\PYG{+w}{ }\PYG{n}{\PYGZus{}}\PYG{o}{,}\PYG{+w}{ }\PYG{k+kd}{by}\PYG{+w}{ }\PYG{n}{decideFin}\PYG{n+nb+bp}{!}\PYG{o}{⟩}
-\end{MintedVerbatim}
diff --git a/paper/_minted/E9660517912C7F2C460C12FB33ED8B81.highlight.minted b/paper/_minted/E9660517912C7F2C460C12FB33ED8B81.highlight.minted
deleted file mode 100644
index cbc072f75..000000000
--- a/paper/_minted/E9660517912C7F2C460C12FB33ED8B81.highlight.minted
+++ /dev/null
@@ -1,16 +0,0 @@
-\begin{MintedVerbatim}[commandchars=\\\{\}]
-\PYG{k+kd}{@[}\PYG{n}{equational\PYGZus{}result}\PYG{k+kd}{]}\PYG{+w}{ }\PYG{k+kn}{theorem}\PYG{+w}{ }\PYG{n}{Equation3973\PYGZus{}implies\PYGZus{}Equation4023}
-\PYG{+w}{    }\PYG{o}{(}\PYG{n}{G}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{k+kt}{Type}\PYG{+w}{ }\PYG{n+nb+bp}{\PYGZus{}}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{[}\PYG{n}{Magma}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{]}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{Equation3973}\PYG{+w}{ }\PYG{n}{G}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{:}\PYG{+w}{ }\PYG{n}{Equation4023}\PYG{+w}{ }\PYG{n}{G}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{k}{fun}\PYG{+w}{ }\PYG{n}{x}\PYG{+w}{ }\PYG{n}{y}\PYG{+w}{ }\PYG{n}{z}\PYG{+w}{ }\PYG{n+nb+bp}{=\PYGZgt{}}
-\PYG{+w}{  }\PYG{k}{let}\PYG{+w}{ }\PYG{n}{v0}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{M}\PYG{+w}{ }\PYG{n}{z}\PYG{+w}{ }\PYG{n}{x}
-\PYG{+w}{  }\PYG{k}{let}\PYG{+w}{ }\PYG{n}{v1}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{M}\PYG{+w}{ }\PYG{n}{z}\PYG{+w}{ }\PYG{n}{v0}
-\PYG{+w}{  }\PYG{k}{let}\PYG{+w}{ }\PYG{n}{v2}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{M}\PYG{+w}{ }\PYG{n}{v1}\PYG{+w}{ }\PYG{n}{y}
-\PYG{+w}{  }\PYG{k}{let}\PYG{+w}{ }\PYG{n}{v3}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{M}\PYG{+w}{ }\PYG{n}{z}\PYG{+w}{ }\PYG{n}{v1}
-\PYG{+w}{  }\PYG{k}{have}\PYG{+w}{ }\PYG{n}{h4}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{R}\PYG{+w}{ }\PYG{n}{v2}
-\PYG{+w}{  }\PYG{k}{have}\PYG{+w}{ }\PYG{n}{h5}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{R}\PYG{+w}{ }\PYG{n}{z}
-\PYG{+w}{  }\PYG{k}{have}\PYG{+w}{ }\PYG{n}{h6}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{h}\PYG{+w}{ }\PYG{n}{z}\PYG{+w}{ }\PYG{n}{x}\PYG{+w}{ }\PYG{n}{v1}
-\PYG{+w}{  }\PYG{k}{let}\PYG{+w}{ }\PYG{n}{v7}\PYG{+w}{ }\PYG{o}{:=}\PYG{+w}{ }\PYG{n}{M}\PYG{+w}{ }\PYG{n}{x}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{M}\PYG{+w}{ }\PYG{n}{v1}\PYG{+w}{ }\PYG{n}{z}\PYG{o}{)}
-\PYG{+w}{  }\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{n}{x}\PYG{+w}{ }\PYG{n}{y}\PYG{+w}{ }\PYG{n}{z}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{M}\PYG{+w}{ }\PYG{n}{y}\PYG{+w}{ }\PYG{n}{v0}\PYG{o}{)}\PYG{+w}{ }\PYG{n}{z}\PYG{+w}{ }\PYG{n}{v2}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{C}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{C}\PYG{+w}{ }\PYG{n}{h5}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{C}\PYG{+w}{ }\PYG{n}{h4}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{n}{y}\PYG{+w}{ }\PYG{n}{v0}\PYG{+w}{ }\PYG{n}{v2}\PYG{o}{)}
-\PYG{+w}{  }\PYG{o}{(}\PYG{n}{C}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{C}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{n}{h6}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{n}{v7}\PYG{+w}{ }\PYG{n}{v1}\PYG{+w}{ }\PYG{n}{v0}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{C}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{C}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{R}\PYG{+w}{ }\PYG{n}{v1}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{T}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{n}{v0}\PYG{+w}{ }\PYG{n}{v7}\PYG{+w}{ }\PYG{n}{z}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{C}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{S}\PYG{+w}{ }\PYG{n}{h6}\PYG{o}{)}\PYG{+w}{ }\PYG{n}{h5}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}
-\PYG{+w}{  }\PYG{o}{(}\PYG{n}{R}\PYG{+w}{ }\PYG{n}{v0}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{S}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{n}{z}\PYG{+w}{ }\PYG{n}{v1}\PYG{+w}{ }\PYG{n}{v0}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{R}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{M}\PYG{+w}{ }\PYG{n}{v2}\PYG{+w}{ }\PYG{n}{y}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{n}{h4}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{S}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{n}{y}\PYG{+w}{ }\PYG{n}{v3}\PYG{+w}{ }\PYG{n}{v2}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{n}{h4}\PYG{o}{)}\PYG{o}{)}
-\PYG{+w}{  }\PYG{o}{(}\PYG{n}{S}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{M}\PYG{+w}{ }\PYG{n}{y}\PYG{+w}{ }\PYG{n}{v3}\PYG{o}{)}\PYG{+w}{ }\PYG{n}{z}\PYG{+w}{ }\PYG{n}{v2}\PYG{o}{)}\PYG{o}{)}\PYG{o}{)}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{S}\PYG{+w}{ }\PYG{o}{(}\PYG{n}{h}\PYG{+w}{ }\PYG{n}{v1}\PYG{+w}{ }\PYG{n}{y}\PYG{+w}{ }\PYG{n}{z}\PYG{o}{)}\PYG{o}{)}
-\end{MintedVerbatim}
diff --git a/paper/_minted/_FAD58DE7366495DB4650CFEFAC2FCD61.index.minted b/paper/_minted/_FAD58DE7366495DB4650CFEFAC2FCD61.index.minted
deleted file mode 100644
index 52b27083e..000000000
--- a/paper/_minted/_FAD58DE7366495DB4650CFEFAC2FCD61.index.minted
+++ /dev/null
@@ -1,13 +0,0 @@
-{
-  "jobname": "main",
-  "md5": "FAD58DE7366495DB4650CFEFAC2FCD61",
-  "timestamp": "20251215124021",
-  "cachefiles": [
-    "12ADCD03C9A93E8738E3EF4CAE987AEF.highlight.minted",
-    "1FC85BECB7EF9A894AC6562535195B40.highlight.minted",
-    "336A906F6F62E71684EE6F94801D4C64.highlight.minted",
-    "E9660517912C7F2C460C12FB33ED8B81.highlight.minted",
-    "_FAD58DE7366495DB4650CFEFAC2FCD61.index.minted",
-    "default.style.minted"
-  ]
-}
\ No newline at end of file
diff --git a/paper/_minted/default.style.minted b/paper/_minted/default.style.minted
deleted file mode 100644
index 3553f35b6..000000000
--- a/paper/_minted/default.style.minted
+++ /dev/null
@@ -1,100 +0,0 @@
-\makeatletter
-\def\PYG@reset{\let\PYG@it=\relax \let\PYG@bf=\relax%
-    \let\PYG@ul=\relax \let\PYG@tc=\relax%
-    \let\PYG@bc=\relax \let\PYG@ff=\relax}
-\def\PYG@tok#1{\csname PYG@tok@#1\endcsname}
-\def\PYG@toks#1+{\ifx\relax#1\empty\else%
-    \PYG@tok{#1}\expandafter\PYG@toks\fi}
-\def\PYG@do#1{\PYG@bc{\PYG@tc{\PYG@ul{%
-    \PYG@it{\PYG@bf{\PYG@ff{#1}}}}}}}
-\def\PYG#1#2{\PYG@reset\PYG@toks#1+\relax+\PYG@do{#2}}
-
-\@namedef{PYG@tok@w}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.73,0.73}{##1}}}
-\@namedef{PYG@tok@c}{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
-\@namedef{PYG@tok@cp}{\def\PYG@tc##1{\textcolor[rgb]{0.61,0.40,0.00}{##1}}}
-\@namedef{PYG@tok@k}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@kp}{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@kt}{\def\PYG@tc##1{\textcolor[rgb]{0.69,0.00,0.25}{##1}}}
-\@namedef{PYG@tok@o}{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
-\@namedef{PYG@tok@ow}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
-\@namedef{PYG@tok@nb}{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@nf}{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
-\@namedef{PYG@tok@nc}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
-\@namedef{PYG@tok@nn}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
-\@namedef{PYG@tok@ne}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.80,0.25,0.22}{##1}}}
-\@namedef{PYG@tok@nv}{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
-\@namedef{PYG@tok@no}{\def\PYG@tc##1{\textcolor[rgb]{0.53,0.00,0.00}{##1}}}
-\@namedef{PYG@tok@nl}{\def\PYG@tc##1{\textcolor[rgb]{0.46,0.46,0.00}{##1}}}
-\@namedef{PYG@tok@ni}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.44,0.44,0.44}{##1}}}
-\@namedef{PYG@tok@na}{\def\PYG@tc##1{\textcolor[rgb]{0.41,0.47,0.13}{##1}}}
-\@namedef{PYG@tok@nt}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@nd}{\def\PYG@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
-\@namedef{PYG@tok@s}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@sd}{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@si}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.64,0.35,0.47}{##1}}}
-\@namedef{PYG@tok@se}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.67,0.36,0.12}{##1}}}
-\@namedef{PYG@tok@sr}{\def\PYG@tc##1{\textcolor[rgb]{0.64,0.35,0.47}{##1}}}
-\@namedef{PYG@tok@ss}{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
-\@namedef{PYG@tok@sx}{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@m}{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
-\@namedef{PYG@tok@gh}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
-\@namedef{PYG@tok@gu}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.50,0.00,0.50}{##1}}}
-\@namedef{PYG@tok@gd}{\def\PYG@tc##1{\textcolor[rgb]{0.63,0.00,0.00}{##1}}}
-\@namedef{PYG@tok@gi}{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.52,0.00}{##1}}}
-\@namedef{PYG@tok@gr}{\def\PYG@tc##1{\textcolor[rgb]{0.89,0.00,0.00}{##1}}}
-\@namedef{PYG@tok@ge}{\let\PYG@it=\textit}
-\@namedef{PYG@tok@gs}{\let\PYG@bf=\textbf}
-\@namedef{PYG@tok@ges}{\let\PYG@bf=\textbf\let\PYG@it=\textit}
-\@namedef{PYG@tok@gp}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
-\@namedef{PYG@tok@go}{\def\PYG@tc##1{\textcolor[rgb]{0.44,0.44,0.44}{##1}}}
-\@namedef{PYG@tok@gt}{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.27,0.87}{##1}}}
-\@namedef{PYG@tok@err}{\def\PYG@bc##1{{\setlength{\fboxsep}{\string -\fboxrule}\fcolorbox[rgb]{1.00,0.00,0.00}{1,1,1}{\strut ##1}}}}
-\@namedef{PYG@tok@kc}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@kd}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@kn}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@kr}{\let\PYG@bf=\textbf\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@bp}{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
-\@namedef{PYG@tok@fm}{\def\PYG@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
-\@namedef{PYG@tok@vc}{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
-\@namedef{PYG@tok@vg}{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
-\@namedef{PYG@tok@vi}{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
-\@namedef{PYG@tok@vm}{\def\PYG@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
-\@namedef{PYG@tok@sa}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@sb}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@sc}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@dl}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@s2}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@sh}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@s1}{\def\PYG@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
-\@namedef{PYG@tok@mb}{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
-\@namedef{PYG@tok@mf}{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
-\@namedef{PYG@tok@mh}{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
-\@namedef{PYG@tok@mi}{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
-\@namedef{PYG@tok@il}{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
-\@namedef{PYG@tok@mo}{\def\PYG@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
-\@namedef{PYG@tok@ch}{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
-\@namedef{PYG@tok@cm}{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
-\@namedef{PYG@tok@cpf}{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
-\@namedef{PYG@tok@c1}{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
-\@namedef{PYG@tok@cs}{\let\PYG@it=\textit\def\PYG@tc##1{\textcolor[rgb]{0.24,0.48,0.48}{##1}}}
-
-\def\PYGZbs{\char`\\}
-\def\PYGZus{\char`\_}
-\def\PYGZob{\char`\{}
-\def\PYGZcb{\char`\}}
-\def\PYGZca{\char`\^}
-\def\PYGZam{\char`\&}
-\def\PYGZlt{\char`\<}
-\def\PYGZgt{\char`\>}
-\def\PYGZsh{\char`\#}
-\def\PYGZpc{\char`\%}
-\def\PYGZdl{\char`\$}
-\def\PYGZhy{\char`\-}
-\def\PYGZsq{\char`\'}
-\def\PYGZdq{\char`\"}
-\def\PYGZti{\char`\~}
-% for compatibility with earlier versions
-\def\PYGZat{@}
-\def\PYGZlb{[}
-\def\PYGZrb{]}
-\makeatother
diff --git a/paper/automated.tex b/paper/automated.tex
index 64e7f4638..fe4eb6b1a 100644
--- a/paper/automated.tex
+++ b/paper/automated.tex
@@ -129,7 +129,6 @@ \subsubsection{Proof Reconstruction}
 \caption{Example of a proof reconstructed by \emph{MagmaEgg}. Note the proof only uses reflexivity, symmetry, transitivity, and congruence of equality.}
 \label{fig:magma-egg-example}
 \end{figure}
-% \todo{Use listings or minted for this code block.}
 
 In the case of the \texttt{egg} tactic, which also reconstructs proofs from \emph{egg} explanations, the proof could be converted into a more human-readable form by using the \texttt{calcify}\footnote{\url{https://github.com/nomeata/lean-calcify}} tactic, as shown in \Cref{fig:egg-example}
 
diff --git a/paper/foundations.tex b/paper/foundations.tex
index 3a715b314..84a0b5083 100644
--- a/paper/foundations.tex
+++ b/paper/foundations.tex
@@ -51,9 +51,9 @@ \section{Formal foundations}
     ∃ (G : Type) (_ : Magma G), Equation1437 G ∧ ¬ Equation4269 G := by
   use ℕ × Fin 3, ⟨op⟩
   constructor
-  ⬝ intro x y z
+  · intro x y z
     simp [op, add_assoc]
-  ⬝ simp only [not_forall, op]
+  · simp only [not_forall, op]
     use (0, 0), (2, 0)
     decide
 \end{lean}
@@ -65,16 +65,16 @@ \section{Formal foundations}
 
 \begin{figure}
 \centering
-\begin{minted}[escapeinside=||]{lean}
+\begin{lean}
 @[equational_result]
-theorem |\textnormal{\guillemotleft}|Facts from All4x4Tables [[1,2,3,4,5,0],[4,1,2,5,0,3],[3,0,5,2,1,4],
-[0,5,4,3,2,1],[5,4,1,0,3,2],[2,3,0,1,4,5]]|\textnormal{\guillemotright}| :
+theorem «Facts from All4x4Tables [[1,2,3,4,5,0],[4,1,2,5,0,3],[3,0,5,2,1,4],
+[0,5,4,3,2,1],[5,4,1,0,3,2],[2,3,0,1,4,5]]» :
   ∃ (G : Type) (_ : Magma G) (_ : Finite G), Facts G [1316, 2863] [411, 680,
   817, 1020, 1426, 2035, 2441, 2644, 2853, 2855, 2865, 2872, 2947, 3050,
   3253, 3456, 4270, 4283, 4290, 4380, 4598, 4605, 4656] :=
-⟨Fin 6, |\textnormal{\guillemotleft}|All4x4Tables [[1,2,3,4,5,0],[4,1,2,5,0,3],[3,0,5,2,1,4],[0,5,4,3,2,1],
-[5,4,1,0,3,2],[2,3,0,1,4,5]]|\textnormal{\guillemotright}|, Finite.of_fintype _, by decideFin!⟩
-\end{minted}
+⟨Fin 6, «All4x4Tables [[1,2,3,4,5,0],[4,1,2,5,0,3],[3,0,5,2,1,4],[0,5,4,3,2,1],
+[5,4,1,0,3,2],[2,3,0,1,4,5]]», Finite.of_fintype _, by decideFin!⟩
+\end{lean}
 \caption{A computer generated \texttt{Facts} theorem, using an explicit finite magma of order $6$ to refute several implications at once.}
 \label{fig:facts}
 \end{figure}
diff --git a/paper/lstlean.tex b/paper/lstlean.tex
new file mode 100644
index 000000000..c6c02e572
--- /dev/null
+++ b/paper/lstlean.tex
@@ -0,0 +1,289 @@
+% Listing style definition for the Lean Theorem Prover.
+% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style.
+% Unicode replacements taken from Olivier Verdier's unixode.sty
+
+\lstdefinelanguage{lean} {
+
+% Anything between $ becomes LaTeX math mode
+mathescape=false,
+% Comments may or not include Latex commands
+texcl=false,
+
+% keywords, list taken from lean-syntax.el
+morekeywords=[1]{
+import, prelude, protected, private, noncomputable, definition, meta, renaming,
+hiding, parameter, parameters, begin, constant, constants,
+lemma, variable, variables, theory,
+print, theorem, example,
+open, as, export, override, axiom, axioms, inductive, with,
+structure, record, universe, universes,
+alias, help, precedence, reserve, declare_trace, add_key_equivalence,
+match, infix, infixl, infixr, notation, postfix, prefix, instance,
+eval, reduce, check, end, this,
+using, using_well_founded, namespace, section,
+attribute, local, set_option, extends, include, omit, class,
+raw, replacing,
+calc, have, show, suffices, by, in, at, let, forall, Pi, fun,
+exists, if, dif, then, else, assume, obtain, from, register_simp_ext, unless, break, continue,
+mutual, do, def, run_cmd, const,
+partial, mut, where, macro, syntax, deriving,
+return, try, catch, for, macro_rules, declare_syntax_cat, abbrev},
+
+% Sorts
+morekeywords=[2]{Sort, Type, Prop},
+
+% tactics, list taken from lean-syntax.el
+morekeywords=[3]{
+assumption,
+apply, intro, intros, allGoals,
+generalize, clear, revert, done, exact,
+refine, repeat, cases, rewrite, rw,
+simp, simp_all, contradiction,
+constructor, injection,
+induction,
+},
+
+% modifiers, taken from lean-syntax.el
+% note: 'otherkeywords' is needed because these use a different symbol.
+% this command doesn't allow us to specify a number -- they are put with [1]
+% otherkeywords={
+% [persistent], [notation], [visible], [instance], [trans_instance],
+% [class], [parsing-only], [coercion], [unfold_full], [constructor],
+% [reducible], [irreducible], [semireducible], [quasireducible], [wf],
+% [whnf], [multiple_instances], [none], [decl], [declaration],
+% [relation], [symm], [subst], [refl], [trans], [simp], [congr], [unify],
+% [backward], [forward], [no_pattern], [begin_end], [tactic], [abbreviation],
+% [reducible], [unfold], [alias], [eqv], [intro], [intro!], [elim], [grinder],
+% [localrefinfo], [recursor]
+% },
+
+% Various symbols
+literate=
+{α}{{\ensuremath{\mathrm{\alpha}}}}1
+{β}{{\ensuremath{\mathrm{\beta}}}}1
+{γ}{{\ensuremath{\mathrm{\gamma}}}}1
+{δ}{{\ensuremath{\mathrm{\delta}}}}1
+{ε}{{\ensuremath{\mathrm{\varepsilon}}}}1
+{ζ}{{\ensuremath{\mathrm{\zeta}}}}1
+{η}{{\ensuremath{\mathrm{\eta}}}}1
+{θ}{{\ensuremath{\mathrm{\theta}}}}1
+{ι}{{\ensuremath{\mathrm{\iota}}}}1
+{κ}{{\ensuremath{\mathrm{\kappa}}}}1
+{μ}{{\ensuremath{\mathrm{\mu}}}}1
+{ν}{{\ensuremath{\mathrm{\nu}}}}1
+{ξ}{{\ensuremath{\mathrm{\xi}}}}1
+{π}{{\ensuremath{\mathrm{\mathnormal{\pi}}}}}1
+{ρ}{{\ensuremath{\mathrm{\rho}}}}1
+{σ}{{\ensuremath{\mathrm{\sigma}}}}1
+{τ}{{\ensuremath{\mathrm{\tau}}}}1
+{φ}{{\ensuremath{\mathrm{\varphi}}}}1
+{χ}{{\ensuremath{\mathrm{\chi}}}}1
+{ψ}{{\ensuremath{\mathrm{\psi}}}}1
+{ω}{{\ensuremath{\mathrm{\omega}}}}1
+
+{Γ}{{\ensuremath{\mathrm{\Gamma}}}}1
+{Δ}{{\ensuremath{\mathrm{\Delta}}}}1
+{Θ}{{\ensuremath{\mathrm{\Theta}}}}1
+{Λ}{{\ensuremath{\mathrm{\Lambda}}}}1
+{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1
+{Φ}{{\ensuremath{\mathrm{\Phi}}}}1
+{Ξ}{{\ensuremath{\mathrm{\Xi}}}}1
+{Ψ}{{\ensuremath{\mathrm{\Psi}}}}1
+{Ω}{{\ensuremath{\mathrm{\Omega}}}}1
+
+{ℵ}{{\ensuremath{\aleph}}}1
+
+{≤}{{\ensuremath{\leq}}}1
+{≥}{{\ensuremath{\geq}}}1
+{≠}{{\ensuremath{\neq}}}1
+{≈}{{\ensuremath{\approx}}}1
+{≡}{{\ensuremath{\equiv}}}1
+{≃}{{\ensuremath{\simeq}}}1
+
+{≤}{{\ensuremath{\leq}}}1
+{≥}{{\ensuremath{\geq}}}1
+
+{∂}{{\ensuremath{\partial}}}1
+{∆}{{\ensuremath{\triangle}}}1 % or \laplace?
+
+{∫}{{\ensuremath{\int}}}1
+{∑}{{\ensuremath{\mathrm{\Sigma}}}}1
+{Π}{{\ensuremath{\mathrm{\Pi}}}}1
+
+{⊥}{{\ensuremath{\perp}}}1
+{∞}{{\ensuremath{\infty}}}1
+{∂}{{\ensuremath{\partial}}}1
+
+{∓}{{\ensuremath{\mp}}}1
+{±}{{\ensuremath{\pm}}}1
+{×}{{\ensuremath{\times}}}1
+
+{⊕}{{\ensuremath{\oplus}}}1
+{⊗}{{\ensuremath{\otimes}}}1
+{⊞}{{\ensuremath{\boxplus}}}1
+
+{∇}{{\ensuremath{\nabla}}}1
+{√}{{\ensuremath{\sqrt}}}1
+
+{⬝}{{\ensuremath{\cdot}}}1
+{•}{{\ensuremath{\cdot}}}1
+{∘}{{\ensuremath{\circ}}}1
+
+%{⁻}{{\ensuremath{^{\textup{\kern1pt\rule{2pt}{0.3pt}\kern-1pt}}}}}1
+{⁻}{{\ensuremath{^{-}}}}1
+{▸}{{\ensuremath{\blacktriangleright}}}1
+
+{∧}{{\ensuremath{\wedge}}}1
+{∨}{{\ensuremath{\vee}}}1
+{¬}{{\ensuremath{\neg}}}1
+{⊢}{{\ensuremath{\vdash}}}1
+
+%{⟨}{{\ensuremath{\left\langle}}}1
+%{⟩}{{\ensuremath{\right\rangle}}}1
+{⟨}{{\ensuremath{\langle}}}1
+{⟩}{{\ensuremath{\rangle}}}1
+
+{↦}{{\ensuremath{\mapsto}}}1
+{←}{{\ensuremath{\leftarrow}}}1
+{<-}{{\ensuremath{\leftarrow}}}1
+{→}{{\ensuremath{\rightarrow}}}1
+{↔}{{\ensuremath{\leftrightarrow}}}1
+{⇒}{{\ensuremath{\Rightarrow}}}1
+{⟹}{{\ensuremath{\Longrightarrow}}}1
+{⇐}{{\ensuremath{\Leftarrow}}}1
+{⟸}{{\ensuremath{\Longleftarrow}}}1
+
+{∩}{{\ensuremath{\cap}}}1
+{∪}{{\ensuremath{\cup}}}1
+{⊂}{{\ensuremath{\subseteq}}}1
+{⊆}{{\ensuremath{\subseteq}}}1
+{⊄}{{\ensuremath{\nsubseteq}}}1
+{⊈}{{\ensuremath{\nsubseteq}}}1
+{⊃}{{\ensuremath{\supseteq}}}1
+{⊇}{{\ensuremath{\supseteq}}}1
+{⊅}{{\ensuremath{\nsupseteq}}}1
+{⊉}{{\ensuremath{\nsupseteq}}}1
+{∈}{{\ensuremath{\in}}}1
+{∉}{{\ensuremath{\notin}}}1
+{∋}{{\ensuremath{\ni}}}1
+{∌}{{\ensuremath{\notni}}}1
+{∅}{{\ensuremath{\emptyset}}}1
+
+{∖}{{\ensuremath{\setminus}}}1
+{†}{{\ensuremath{\dag}}}1
+
+{ℕ}{{\ensuremath{\mathbb{N}}}}1
+{ℤ}{{\ensuremath{\mathbb{Z}}}}1
+{ℝ}{{\ensuremath{\mathbb{R}}}}1
+{ℚ}{{\ensuremath{\mathbb{Q}}}}1
+{ℂ}{{\ensuremath{\mathbb{C}}}}1
+{⌞}{{\ensuremath{\llcorner}}}1
+{⌟}{{\ensuremath{\lrcorner}}}1
+{⦃}{{\ensuremath{\{\!|}}}1
+{⦄}{{\ensuremath{|\!\}}}}1
+
+{‖}{{\ensuremath{\|}}}1
+{₁}{{\ensuremath{_1}}}1
+{₂}{{\ensuremath{_2}}}1
+{₃}{{\ensuremath{_3}}}1
+{₄}{{\ensuremath{_4}}}1
+{₅}{{\ensuremath{_5}}}1
+{₆}{{\ensuremath{_6}}}1
+{₇}{{\ensuremath{_7}}}1
+{₈}{{\ensuremath{_8}}}1
+{₉}{{\ensuremath{_9}}}1
+{₀}{{\ensuremath{_0}}}1
+{ᵢ}{{\ensuremath{_i}}}1
+{ⱼ}{{\ensuremath{_j}}}1
+{ₐ}{{\ensuremath{_a}}}1
+
+{¹}{{\ensuremath{^1}}}1
+
+{ₙ}{{\ensuremath{_n}}}1
+{ₘ}{{\ensuremath{_m}}}1
+{ₚ}{{\ensuremath{_p}}}1
+{↑}{{\ensuremath{\uparrow}}}1
+{↓}{{\ensuremath{\downarrow}}}1
+
+{...}{{\ensuremath{\ldots}}}1
+{·}{{\ensuremath{\cdot}}}1
+
+{▸}{{\ensuremath{\triangleright}}}1
+
+{Σ}{{\color{symbolcolor}\ensuremath{\Sigma}}}1
+{Π}{{\color{symbolcolor}\ensuremath{\Pi}}}1
+{∀}{{\color{symbolcolor}\ensuremath{\forall}}}1
+{∃}{{\color{symbolcolor}\ensuremath{\exists}}}1
+{λ}{{\color{symbolcolor}\ensuremath{\mathrm{\lambda}}}}1
+{\$}{{\color{symbolcolor}\$}}1
+
+{:=}{{\color{symbolcolor}:=}}1
+{=}{{\color{symbolcolor}=}}1
+{<|>}{{\color{symbolcolor}<|>}}1
+{<\$>}{{\color{symbolcolor}<\$>}}1
+{+}{{\color{symbolcolor}+}}1
+{*}{{\color{symbolcolor}*}}1,
+
+% Comments
+%comment=[s][\itshape \color{commentcolor}]{/-}{-/},
+morecomment=[s][\color{commentcolor}]{/-}{-/},
+morecomment=[l][\itshape \color{commentcolor}]{--},
+
+% Spaces are not displayed as a special character
+showstringspaces=false,
+
+% keep spaces
+keepspaces=true,
+
+% String delimiters
+morestring=[b]",
+morestring=[d]’,
+
+% Size of tabulations
+tabsize=3,
+
+% Enables ASCII chars 128 to 255
+extendedchars=false,
+
+% Case sensitivity
+sensitive=true,
+
+% Automatic breaking of long lines
+breaklines=true,
+breakatwhitespace=true,
+
+% Default style fors listingsred
+basicstyle=\ttfamily\small,
+
+% Position of captions is bottom
+captionpos=b,
+
+% Full flexible columns
+columns=[l]fullflexible,
+
+
+% Style for (listings') identifiers
+identifierstyle={\ttfamily\color{black}},
+% Note : highlighting of Coq identifiers is done through a new
+% delimiter definition through an lstset at the beginning of the
+% document. Don't know how to do better.
+
+% Style for declaration keywords
+keywordstyle=[1]{\ttfamily\color{keywordcolor}},
+
+% Style for sorts
+keywordstyle=[2]{\ttfamily\color{sortcolor}},
+
+% Style for tactics keywords
+keywordstyle=[3]{\ttfamily\color{tacticcolor}},
+
+% Style for attributes
+keywordstyle=[4]{\ttfamily\color{attributecolor}},
+
+% Style for strings
+stringstyle=\ttfamily,
+
+% Style for comments
+commentstyle={\ttfamily\footnotesize },
+
+}
diff --git a/paper/main.tex b/paper/main.tex
index c42d017e6..cf19d7284 100644
--- a/paper/main.tex
+++ b/paper/main.tex
@@ -32,27 +32,20 @@
   semi/.style    = {->, thick, dash pattern=on 4pt off 2pt on 1pt off 2pt, color=black!80, shorten >=1pt}
 }
 
-% Setup for `minted`
-\usepackage{minted}
-\newminted[lean]{lean4}{fontsize=\small}
-\newmintinline[leaninline]{lean4}{fontsize=\small}
+\usepackage{listings}
+\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
+\definecolor{tacticcolor}{rgb}{0.0, 0.1, 0.6}    % blue
+\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
+\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
+\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
+\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red
+\def\lstlanguagefiles{lstlean.tex}
+\lstnewenvironment{lean}{\lstset{language=lean}}{}
+\DeclareUnicodeCharacter{25C7}{$\diamond$}
 
 \usepackage[hidelinks]{hyperref}
 \usepackage{cleveref}
 
-% Setup for unicode characters in code (minted) blocks.
-\usepackage{newunicodechar}
-\newunicodechar{∃}{$\exists$}
-\newunicodechar{∧}{$\wedge$}
-\newunicodechar{⬝}{$\cdot$}
-\newunicodechar{ℕ}{$\mathbb{N}$}
-\newunicodechar{¬}{$\neg$}
-\newunicodechar{×}{$\times$}
-\newunicodechar{⟨}{$\langle$}
-\newunicodechar{⟩}{$\rangle$}
-\newunicodechar{≠}{$\ne$}
-\newunicodechar{◇}{$\diamond$}
-
 % Page Setup
 \geometry{letterpaper, margin=1in}
 \setlength{\parindent}{0pt} % No indent for paragraphs