WIP: Documentation on Iris equalities
This document tries to document the subtleties involved in Iris equalities. To be somewhat self-contained, it also explains a few subtleties about how Iris-on-paper maps into Iris-coq, but only as needed.
@jung took a look at an earlier version, and suggested a few more points to discuss; FWIW, the early history is in https://gist.github.com/Blaisorblade/855b5c99b3827c306433c6da4cb689c5.
Please feel free to edit directly as you see fit; and let's maybe go through high-level concerns before the details.