The diagonal lemma can be carried out uniformly: from a one-variable formulacode, compute a sentence code whose assertion is equivalent to the original formula applied to that sentence code. The effective substitution operation is what turns a semantic diagonal argument into a productive function.
