Things to describe not in the original quotient paper:

* Type maps and Relation maps (show the case for functions)
* Quotient extensions
* Respectfulness and preservation
  - Show special cases for quantifiers and lambda
* Quotient-type locale
  - Show the proof as much simpler than Homeier's one
* Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)
* Lifting vs Descending vs quot_lifted
  - automatic theorem translation heuristic
* Partial equivalence quotients
  - Bounded abstraction
  - Respects
  - partial_descending
* The heuristics for automatic regularization, injection and cleaning.
* A complete example of a lifted theorem together with the regularized
  injected and cleaned statement
* Examples of quotients and properties that we used the package for.
* co/contra-variance from Ondrej should be taken into account