diff --git a/spec/rule_list.tex b/spec/rule_list.tex index 20d98162da775a1900b470437d13fa96d94e5f35..5f0decf14c5e25263eca434b3222b4c39923b2de 100644 --- a/spec/rule_list.tex +++ b/spec/rule_list.tex @@ -410,17 +410,19 @@ the context. Either \begin{plContainer} \begin{plList} -\Gamma\proofsep& i.& t_1 \simeq t_2 &(\dots)\\ -\Gamma\proofsep& j.& t_2 \simeq t_3 &(\dots)\\ -\Gamma\proofsep& k.& t_1 \simeq t_3 &(\currule; i, j)\\ +\Gamma\proofsep& i_1.& t_1 \simeq t_2 &(\dots)\\ +\Gamma\proofsep& i_2.& t_2 \simeq t_3 &(\dots)\\ +\Gamma\proofsep& i_n.& t_n \simeq t_{n+1} &(\dots)\\ +\Gamma\proofsep& j.& t_1 \simeq t_{n+1} &(\currule; i_1, \dots, i_n, j)\\ \end{plList} \end{plContainer} or \begin{plContainer} \begin{plList} -\Gamma\proofsep& i.& \varphi_1 \leftrightarrow \varphi_2 &(\dots)\\ -\Gamma\proofsep& j.& \varphi_2 \leftrightarrow \varphi_3 &(\dots)\\ -\Gamma\proofsep& k.& \varphi_1 \leftrightarrow \varphi_3 &(\currule; i, j)\\ +\Gamma\proofsep& i_1.& \varphi_1 \leftrightarrow \varphi_2 &(\dots)\\ +\Gamma\proofsep& i_2.& \varphi_2 \leftrightarrow \varphi_3 &(\dots)\\ +\Gamma\proofsep& i_n.& \varphi_n \leftrightarrow \varphi_{n+1} &(\dots)\\ +\Gamma\proofsep& j.& \varphi_1 \leftrightarrow \varphi_{n+1} &(\currule; i_1,\dots, i_n, j)\\ \end{plList} \end{plContainer}