Added support for elimination of defined connectives.
Added some notes about consistency of narrative.
Small refactorings.