Given you want to “push the diagonal lemma around / hide it somewhere” and come up with something equivalent but with another shape (I share Nate’s intuitions), something like this paper’s appendix (§12) might be useful: they build the diagonal lemma directly into the Gödel numbering. This might allow for defining your desired proof by a formula and trivially obtaining existence (and your target audience won’t need to know weird stuff happened inside the Gödel numbering). I’ll try to work this out in the near future.
Given you want to “push the diagonal lemma around / hide it somewhere” and come up with something equivalent but with another shape (I share Nate’s intuitions), something like this paper’s appendix (§12) might be useful: they build the diagonal lemma directly into the Gödel numbering. This might allow for defining your desired proof by a formula and trivially obtaining existence (and your target audience won’t need to know weird stuff happened inside the Gödel numbering). I’ll try to work this out in the near future.