diff --git a/spec/changelog.tex b/spec/changelog.tex
index 50e52bc253136a8f9d86f45b65afb2730845765a..3ff625899a52be0c1bec08067343ef10d3e84903 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -16,6 +16,9 @@ Breaking changes:
   \item Add the sort to all variables in contexts.  Before, the context
         of a bind could be \texttt{(x S) (:= y x)}.  Now it must
         be \texttt{(x S) (:= (y S) x)}.
+  \item The arguments for \proofRule{forall_inst} have been changed to
+        no longer take the shape of bindings using \texttt{(:= x c)}.
+        Instead, the list of instatiation terms must follow the variable order and cover all the respective bound variables.
 \end{itemize}
 
 \noindent
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 6e6977a06c1c1ada7c914762b14a695aa70b0ae6..2d707d17c05ca3380a78e89352174e39d4811b28 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -670,15 +670,22 @@ $k$. & $\Gamma$ & \ctxsep  & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \curru
 \begin{AletheX}
 $i$. & \ctxsep &
 $\neg (\forall x_1, \dots, x_n. P) \lor P[x_1\mapsto t_1]\dots[x_n\mapsto t_n]$
- & \currule\, [$(x_{k_1}, t_{k_1})$, $\dots$, $(x_{k_n}, t_{k_n})$] \\
+ & \currule\, [$t_1$, $\dots$, $t_n$] \\
 \end{AletheX}
 
 \noindent
-where $k_1, \dots, k_n$ is a permutation of $1, \dots, n$ and $x_{k_i}$ and
-$t_{k_i}$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
-\inlineAlethe{(:= xki tki)}.
+where $x_i$ and $t_i$ have the same sort.
 \end{RuleDescription}
 
+\begin{RuleExample}
+An application of the \proofRule{forall_inst} rule.
+\begin{AletheVerb}
+(step t16 (cl (or (not (forall ((x S) (y T)) (P y x    )))
+                                             (P b (f a))
+      :rule forall_inst :args ((f a) b)
+\end{AletheVerb}
+\end{RuleExample}
+
 
 \begin{RuleDescription}{refl}
 \begin{AletheXS}
@@ -1763,7 +1770,7 @@ $j$. & \ctxsep & $ \neg (\psi ≈ \varphi)$  & (\currule\; $i$) \\
 \noindent
 If $\varphi \neq \psi$ then the conclusion \emph{must not} be $\neg (\varphi ≈ \psi)$.
 
-See \ruleref{symm} for an explanation of this rule.
+See \proofRule{symm} for an explanation of this rule.
 
 \end{RuleDescription}