Updated proof documentation.

The proof documentation was missing the rule :distinctBoolEq.  A presentation
of this rule was added.  To this point, no additional documentation is present
since the rule should be self-explanatory.