@@ -109,7 +109,7 @@ The first of these has the following type:
109109*views> :p views.parity_lemma_1
110110
111111---------------------------------- (views.parity_lemma_1) --------
112−{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))
112+{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (j + j)))
113113
114114-views.parity_lemma_1>
115115
@@ -127,7 +127,7 @@ the prelude:
127127\begin{SaveVerbatim}{plusnsm}
128128
129129plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
130− S (plus left right) = plus left (S right)
130+ S (left + right) = left + (S right)
131131
132132
133133\end{SaveVerbatim}
@@ -143,11 +143,26 @@ After applying \texttt{intro} twice, we have:
143143 j : Nat
144144 value : Parity (S (plus j (S j)))
145145---------------------------------- (views.parity_lemma_1) --------
146−{hole2} : Parity (S (S (plus j j)))
146+{hole2} : Parity (S (S (j + j)))
147147
148148\end{SaveVerbatim}
149149\useverb{prolemii}
150150
151+\noindent
152+We need to use \texttt{compute} again to unfold the definition of \texttt{(+)}.
153+
154+\begin{SaveVerbatim}{prolemcomp}
155+
156+-views.parity_lemma_1> intro
157+
158+ j : Nat
159+ value : Parity (S (plus j (S j)))
160+---------------------------------- (views.parity_lemma_1) --------
161+{hole2} : Parity (S (S (plus j j)))
162+
163+\end{SaveVerbatim}
164+\useverb{prolemcomp}
165+
151166\noindent
152167Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
153168to \texttt{j} and \texttt{j}, giving: