Add elimDesc to formalization
Make Mu take Branches parameter.

This makes it possible to support levitation later.