Lachnitt
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
 as for the rule \proofRule{la_generic}.
 \end{RuleDescription}

+\begin{RuleDescription}{la_mult_pos}
+
+Either of the form:
+
+	\begin{AletheX}
+		$i$. & \ctxsep  &
+		 $(t_1 > 0 \wedge t_2 \bowtie t_3) \to t_1 * t_2 \bowtie t_1 * t_3$
-		 $(t_1 > 0 \wedge t_2 \bowtie t_3) \to t_1 * t_2 \bowtie t_1 * t_3$
+		 $(t_1 > 0 \land t_2 \bowtie t_3) \rightarrow t_1 * t_2 \land t_1 * t_3$
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
+	$ \ge $ & $ \le $ \\
+	\hline
+	\end{tabular}
+	\end{center}
+
+\noindent Or of the form:
+
+	\begin{AletheX}
+		$i$. & \ctxsep  &
+		$(t_1 < 0 \wedge \neg (t_2 ≈ t_3)) \to \neg (t_1 * t_2 ≈ t_1 * t_3)$
+		& (\currule) \\
+	\end{AletheX}
+	.
+\end{RuleDescription}
+
+\begin{RuleDescription}{la_totality}