Entertainingly, dub types fit elimination-with-a-motive very nicely. The dub types in a problem get refined along with everything else, leaving the same identifiers in scope, but with more informative definitions. That way, we can reliably stack up a sequence of refinement strategies and be sure that the later strategies still make sense in the scope resulting from the earlier strategies. Once refinement’s done, the business of elaborating the next “left-hand side” is to transform the problem into an equivalent one with more dub types inserted, in accordance with the programmer’s use of pattern variables.

We used to have much more ghastly ways to work on this problem. Epigram 1 relied on choosing a particular α-variant of the goal to make the names in scope fit the programmer’s choices. That such an approach violates several of my own principles about meaning and naming should have been a warning to me earlier…

By the way, is there something to say on how the dubbing assumptions (’x’ : S = s) get used? The post only shows their introduction.

did you mean “checkable term” instead?