-

Ran into a snag with the proof: descending into lambdas
breaks the idea of reducing away all of the iteration
from an almost-closed (i.e. only diamonds are free variables)
term. It might take some time before a counterexample
or workaround reveals itself, I think.