Add bind_let rule

This rule is used by Carcara's elaborator when eliminating the implicit use of symmetry of equality.

Addresses #46

spec/changelog.tex

@@ -13,6 +13,8 @@ Proof rules:
   and tedious use of \proofRule{subproof} for each direction of the equivalence.
   \item Addition of the rule \proofRule{weakening} to express weakening of a
         clause.
+  \item Addition of the \proofRule{reordering} rule to represent reordering of
+        the literals in a clause.
   \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.