We can treat mu and nu formulas the same way in the rules (at first) since we only use the property that these formulas define fixpoints, and at that point is does not matter which particular fix point, since we just unroll the fixpoint. That means if we have x=f(x), we replace x by f(x) that's all. However, note that if a repetition is found, then the treatment of mu and nu is different. At that point we do care about least and greatest fixpoints.
And, yes mu x. phi is always a subset of nu x.phi, since the set of fixpoints form a lattice also.
