The hanfor boggie grammar allows expressions to be empty

[hauff]

That seems to be a work around

• to allow saving empty formalizations
• to parse unused expressions (e.g. P, Q, S, T, U, V in pattern Universality Globally)

Maybe a better solution could be that the grammar does not allow empty expressions, since we don't need to parse them.