partial (co-)Büchi realizability
Taking the same automaton as in #407, let's assume that the condition is not α="(Fin(0)|Fin(1)|Fin(2)) | Inf(3)" but some more complex formula that has α as a subformula. You may also imagine more colors used in the automaton and in the rest of the conditions.
We can still discover that α is Büchi-realizable and replace it with
Inf(x). That would work like partial-degeneralization, but for (co-)Büchi-realizability.