Documentation on Iris equalities (take 2)

To avoid losing all the work that was put into !300 (closed), here's my take on those docs: I did some editing of @Blaisorblade's text, removed a few things that seemed to venture too far off the main story here, and added some remarks that seemed useful.