Update README

Author: jvanbruegge

README.md

@@ -11,28 +11,15 @@ You can find the proof of type safety in [Soundness.thy](./Soundness.thy), the p
 ## Roadmap
 
 -   [x] Start with a simply typed lambda calculus
-    -   [x] Define system
-    -   [x] Prove Progress
-    -   [x] Prove Preservation
 -   [x] Add let bindings
-    -   [x] Extend definition
-    -   [x] Prove Progress
-    -   [x] Prove Preservation
 -   [x] Use the Nominal2 framework to reason about alpha-equated terms
--   [ ] Add datatypes and `case` expressions
-    -   [ ] Extend definition
-    -   [ ] Prove Progress
-    -   [ ] Prove Preservation
 -   [x] Extend to System F (ie introduce polymorphic variables)
-    -   [x] Extend definition
-    -   [x] Prove Progress
-    -   [x] Prove Preservation
--   [ ] Extend System F with Coercions
-    -   [ ] Extend definition
-    -   [ ] Prove Progress
-    -   [ ] Prove Preservation
--   [ ] TBD
+-   [ ] Add arbitrary user-defined datatypes
+-   [ ] Add `case` expressions
+-   [ ] Extend to System Fc (ie introduce type equality coercions)
 
 ## Used literature
 
-Up until now, I mainly used [Software Foundations: Programming Language Foundations](https://softwarefoundations.cis.upenn.edu/current/plf-current/toc.html) and the [System Fc paper](https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf?from=https%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople%2Fsimonpj%2Fpapers%2Fext-f%2Ftldi22-sulzmann-with-appendix.pdf).
+-   [Software Foundations: Programming Language Foundations](https://softwarefoundations.cis.upenn.edu/current/plf-current/toc.html)
+-   [System F with type equality coercions](https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf?from=https%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople%2Fsimonpj%2Fpapers%2Fext-f%2Ftldi22-sulzmann-with-appendix.pdf).
+-   [Safe zero-cost coercions for Haskell](https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf)