Items needed for a paper

[ ] Typecheck DOT examples to argue this is "DOT" enough (#26)
[ ] Technical appendix? Unneeded if the Coq formalization is clean enough. Probably (parts of) stamping goes in there.
[ ] Writing plan/outline

Please help fill in the outline. Items I expect:

Introduction
DOT examples, both to explain DOT, and to argue our DOT variant is DOT-like enough
(Somewhere) examples of issues with the DOT syntax, to motivate why our restrictions make sense regardless of our model. Here we can show cyclic proofs.
Our model. At first, we should tell the reader to ignore all occurrences of later. We can also keep the "implementation" of storing semantic types in values "abstract", similarly to the runST paper. Then, we explain the restrictions. Since this section is about modeling impredicative type members, it should be written for a larger audience if possible.
Later, we explain how we use stored predicates and stamping and wellMapped and whatnot. This section requires familiarity not just with step-indexing but also with Iris, so this section should be encapsulated (again, like for runST).
Some words on the mechanization itself.
Conclusions

Blaisorblade / dot-iris