This also serves as a regression test through our nightly CI builds.
Unfortunately I found only one place where previously it did a dedicated iDestruct ... as %foo and then actually used the name foo. But from a testing perspective that has us covered. ;)
iDestruct ... as %foo
Cc @robbertkrebbers @tchajed