Working on the consistency of environment: list of pairs of count formulas
is now working.
Cleaned up...added a section called Environment.
Added f+q and f-q...
Bunch of changes: hooked up the environment and everything else. Removed
how I was specifying counts (as hyposthesis). Now the counts are built
into the env. Redid most of the theorems. All works fine at this point.
Still need to work on the translation part and build a hierarchy of types
instead of always returning Prop (e.g. need to find the permitted free
formulas).