Document the usage of the next-generation equivalence reasoner

[jeltsch]

This resolves #4.

[javierdiaz72]

Please find below my conclusions of the review:

• I didn’t find any typos or syntactic errors.
• I didn’t find any errors related to antiquotations.
• I have two recommendations aimed to aid the user, namely:
  • I think it would be great to add a minimal example including a custom equivalence relation R, a function f that is compatible with R, and a lemma involving a property of R that can be proved by the equivalence proof method.
  • I think it would be neat to use railroad diagrams to specify the syntax of the equivalence and try_equivalence proof methods.

[jeltsch]

Thank you very much for your thorough review.

I’d like to address your recommendations via separate issues:

• Add an example of using the next-generation equivalence reasoner #16
• Start using railroad diagrams to describe syntax #17

If you’re otherwise happy with this pull request, could you please accept it? Thank you.

[javierdiaz72]

LGTM!