diff --git a/alonzo/formal-spec/utxo.tex b/alonzo/formal-spec/utxo.tex
index a07183ce6ae..1270aca1488 100644
--- a/alonzo/formal-spec/utxo.tex
+++ b/alonzo/formal-spec/utxo.tex
@@ -874,11 +874,10 @@ \subsection{Witnessing}
       \hldiff{\var{inputHashes}\leteq \{ h \mid (\_ \mapsto (a, \_, h)) \in \txins{txb} \restrictdom \var{utxo}, \fun{isTwoPhaseScriptAddress}~{tx}~{a}\}}   \\~\\
       \hldiff{\forall \var{s} \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhOne,
       \fun{validateScript}~\var{s}~\var{tx}}\\~\\
-      \hldiff{\{ s \mid (\_, s) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\
+      \hldiff{\{ h \mid (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\
       \hldiff{\var{inputHashes} \subseteq \dom (\fun{txdats}~{txw})} \\~\\
       \hldiff{\dom (\fun{txdats}~{txw}) \subseteq \var{inputHashes} \cup \{h~\mid~ (\wcard, \wcard, h)\in\fun{txouts}\}}
       \\~\\
-      \hldiff{\forall (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx},~h \in \dom (\fun{txscripts}~(\fun{txwits}~tx))} \\
       \hldiff{\ \dom (\fun{txrdmrs}~tx) ~=~\{~\fun{rdptr}~txb~sp~
        \vert~ (sp,h)~\in~\fun{scriptsNeeded}~\var{utxo}~\var{tx}, } \\
       \hldiff{h\mapsto s~\in~\fun{txscripts}~{txw}, s~\in~\ScriptPhTwo \}}