A variant of DOT, where preservation should hold.

The not-free restrictions in term-mem and new are lifted by hard-coding
subsumption. We lose unicity of types and decidability...