Revert "feat: add Lean4 syntax highlighting support to template"

This reverts commit 14c0d08.

paper.tex

@@ -70,12 +70,10 @@
 {
 \newminted[mlir]{tools/MLIRLexer.py:MLIRLexerOnlyOps}{customlexer, mathescape}
 \newminted[xdsl]{tools/MLIRLexer.py:MLIRLexer}{customlexer, mathescape, style=murphy}
-\newminted[lean4]{tools/Lean4Lexer.py:Lean4Lexer}{customlexer, mathescape}
 }
 {
 \newminted[mlir]{tools/MLIRLexer.py:MLIRLexerOnlyOps -x}{mathescape}
 \newminted[xdsl]{tools/MLIRLexer.py:MLIRLexer -x}{mathescape, style=murphy}
-\newminted[lean4]{tools/Lean4Lexer.py:Lean4Lexer -x}{mathescape}
 }
 \makeatother
 
@@ -132,14 +130,6 @@
 \usepackage{booktabs}
 \newcommand{\ra}[1]{\renewcommand{\arraystretch}{#1}}
 
-\usepackage[verbose]{newunicodechar}
-\newunicodechar{₁}{\ensuremath{_1}}
-\newunicodechar{₂}{\ensuremath{_2}}
-\newunicodechar{∀}{\ensuremath{\forall}}
-\newunicodechar{α}{\ensuremath{\alpha}}
-\newunicodechar{β}{\ensuremath{\beta}}
-
-
 % \circled command to print a colored circle.
 % \circled{1} pretty-prints "(1)"
 % This is useful to refer to labels that are embedded within figures.
@@ -572,20 +562,6 @@ \subsubsection{Listings} We aim to use minted to create listings as much as
 \label{lst:example}
 \end{listing}
 
-\begin{listing}[H]
-\begin{lean4}
-theorem funext {f₁ f₂ : ∀ (x : α), β x}
-  (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
-  show extfunApp (Quotient.mk' f₁) = 
-       extfunApp (Quotient.mk' f₂)
-  apply congrArg
-  apply Quotient.sound
-  exact h
-\end{lean4}
-\caption{A simple Lean4 code example, taken from
-  \url{https://lean-lang.org/lean4/doc/syntax\_highlight\_in\_latex.html\#example-with-minted}.}
-\end{listing}
-
 The syntax highlighting also works for xDSL-like IRs. Notice that different
 minted styles can be used for different environments. The xDSL environment uses
 the murphy-style in this case, whereas the MLIR version applies the