* Get rid of levitatable version.
** It is not mentioned in paper.

* Show how to use ext3
** The 3-argument dependent extensional equality axiom
Get rid of RecFun.

It let's you have recursive function construtor arguments.
We never used it in the paper.