Polymorphic record types in a lifted enbedding - by Stefan Zeiger