Effective diagonal lemma
= Effective diagonal lemma
The <Diagonal lemma> can be carried out uniformly: from a one-variable formula code, 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>.