Add shuffle rule

This adds a shuffle rule to Alethe that can be used to change the order of arguments of commutative operators. Two remarks:

• Reconstruction might be easier if steps using this rules come with a permutation in the arguments. So for example:

(step s1 (= (cl (+ a b c) (+ b a c)) :rule shuffle :args (2 1 3))

However, I am not certain of hard it is to generate this. I suggest we think about adding this after Hanna used this rule.

• We should consider renaming reordering to shuffle_clause. In the proofs meeting yesterday we said that "reorder" is not a good name, because it implies a specific order.

spec/changelog.tex

@@ -18,6 +18,8 @@ Proof rules:
   \item Addition of the \proofRule{bind_let} rule.  This rule can be used to
         preprocess \inlineAlethe{let} expressions similar to the \proofRule{bind}
         rule used with ordinary quantifiers.
+  \item Additon of the \proofRule{shuffle} to permute the arguments of a
+        commutative operator.
 \end{itemize}
 
 \noindent