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

@@ -15,6 +15,9 @@ Proof rules:
         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.
 \end{itemize}
 
 \noindent