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,9 @@ 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{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