Update the readme to describe how this relates to the original version.

README.md

 # Iris + Fair Refinements COQ DEVELOPMENT
 
 This is the Coq development for an extension of Iris to support
-termination-preserving fair refinement. 
+termination-preserving fair refinement. It is an updated version of work
+described in the paper:
+
+    A Higher-Order Logic for Concurrent Termination-Preserving Refinement
+    J. Tassarotti, R. Jung, R. Harper.
+    ESOP 2017
+
+This version makes use of MoSeL, an extension to the earlier Iris Proof Mode to
+support general BI logics.
 
 ## Prerequisites