Started work on PSP submission:

 * Formatting of page 3 is off; Fig 8 should be at the bottom.
 * Proof of Thm 9 is done modulo:
    * "Lemma B" -- list of obvious facts about regexes.
      B(1) = s in r and s' in r' => ss' in rr'
      B(2) = excluded middle for language inclusion
    * "Lemma C", aka subst-replace correspondence theorem

We need some discussion about the meta-theoretic functions ofr replacement and
substitution; their role is non-obvious.