Avoid \verb in command argument

And abstract typesetting the proof term names away. Avoid repetition and
all that nice programming stuff.

tex/paper.mng

@@ -43,6 +43,8 @@
 \newcommand{\eqrefl}{\text{eq-refl~}}
 \newcommand{\secondDP}{\text{second-dp~}}
 
+\newcommand\prooftermname[1]{\texttt{#1}}
+
 \begin{document}
 
 \newNTclass{nonterm}
@@ -303,7 +305,7 @@ We prove some of the usual metatheoretical properties of the proposed language.
 We also provide machine-verified proofs of these theorems in the supplemental code,
 with the corresponding proof terms referred in lemmas statements.
 
-\begin{lemma}[Agreement I, \verb +T-implies-TCTX]\label{lma:term_wf_implies_ctx_wf}
+\begin{lemma}[Agreement I, \prooftermname{T-implies-TCTX}]\label{lma:term_wf_implies_ctx_wf}
   If $[[ G |- es : ts ]]$, then $[[ G ok ]]$.
 \end{lemma}
 \begin{proof}
@@ -312,7 +314,7 @@ with the corresponding proof terms referred in lemmas statements.
   and the other rules recurse on one of their premises.
 \end{proof}
 
-\begin{lemma}[Agreement II, \verb +TWF-implies-TCTX]\label{lma:type_wf_implies_ctx_wf}
+\begin{lemma}[Agreement II, \prooftermname{TWF-implies-TCTX}]\label{lma:type_wf_implies_ctx_wf}
   If $[[ G |- ts ]]$, then $[[G ok]]$.
 \end{lemma}
 \begin{proof}
@@ -325,10 +327,10 @@ with the corresponding proof terms referred in lemmas statements.
 For the following two lemmas,
 assume $[[ G ]]$, $[[ G' ]]$ are contexts such that $[[ G ]] \subset [[ G' ]]$ and $[[ G' ok ]]$.
 Then:
-\begin{lemma}[Thinning on types, \verb +twf-thinning]\label{lma:thinning_twf}
+\begin{lemma}[Thinning on types, \prooftermname{twf-thinning}]\label{lma:thinning_twf}
   If $[[ G |- ts ]]$, then $[[ G' |- ts ]]$.
 \end{lemma}
-\begin{lemma}[Thinning on terms, \verb +t-thinning]\label{lma:thinning_t}
+\begin{lemma}[Thinning on terms, \prooftermname{t-thinning}]\label{lma:thinning_t}
   If $[[ G |- es : ts ]]$, then $[[ G' |- es : ts ]]$.
 \end{lemma}
 These two lemmas are proven using mutual induction,
@@ -352,7 +354,7 @@ this is a well-founded proof.
   then it must conclude $[[ [| G' |] => A v. (r1 => r2) ]]$.
 \end{proof}
 
-\begin{lemma}[Substitution on types, \verb +sub-TWF]\label{lma:type_substitution}
+\begin{lemma}[Substitution on types, \prooftermname{sub-TWF}]\label{lma:type_substitution}
   Assume $[[ G, x : ts, GD |- ts' ]]$ and $[[ G |- es : ts ]]$, then $[[ G, [ x |-> es ] GD |- [ x |-> es ] ts' ]] $.
 \end{lemma}
 \begin{proof}
@@ -361,7 +363,7 @@ this is a well-founded proof.
   We refer the interested reader to the formal proof of theorem in the supplemental code for the specific details.
 \end{proof}
 
-\begin{lemma}[Agreement III, \verb +T-implies-TWF]\label{lma:term_wf_implies_type_wf}
+\begin{lemma}[Agreement III, \prooftermname{T-implies-TWF}]\label{lma:term_wf_implies_type_wf}
   If $[[ G |- es : ts ]]$, then $[[ G |- ts ]]$.
 \end{lemma}
 \begin{proof}