We need to enforce some assumptions for μ-Calculus. Add (still empty) checker function and call them when importing the forumla
