Main paper (version 2020-11-07)

paper-2020-11-07-30b197d9

Write a paragraph about reflecting dependent stuff into oracle world

Main paper (version 2020-11-04)

Avoid \verb in command argument

And abstract typesetting the proof term names away. Avoid repetition and
all that nice programming stuff.

Main paper (version 2020-11-04)

paper-2020-11-04-dbf94169

Remove now-irrelevant todo

Main paper (version 2020-11-04)

paper-2020-11-04-66ea1929

Better missing ref name to mention the subject

Main paper (version 2020-11-04)

paper-2020-11-04-29b81fb3

Better text style

Main paper (version 2020-10-20)

paper-2020-10-20-f8ab8a46

A tad better text style

Main paper (version 2020-10-13)

paper-2020-10-13-38456c1b

Better formulation of the commutativity theorem in overview

Main paper (version 2020-10-12)

paper-2020-10-12-d44242f6

Surface progress and preservation doesn't follow from the ~~>-equival…

Main paper (version 2020-09-24)

paper-2020-09-24-7b77365d

Define substitutions on core expressions

Main paper (version 2020-09-23)

paper-2020-09-23-bedcb43a

More consistent naming