Use COFEs only for the recursive domain equation solver

This fact is deduced from reducibility. Unfortunately, this sometimes depends on the type of states being inhabited, so that this additional hypothesis sometimes appear.