Implement modal cube
In Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare Dixon: Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic (CADE 2023) there are encodings of the modal cube into K. It might be worth investigating whether this extends to our fixpoint calculi.