Add inverse functions for all parsing rules. Further simplify parsing
of binder formulas and factor out toplevel (iff, implies) connector
formulas to make printing implementation easier.