Initial part of abbreviations mechanism

Still very much incomplete, with the following yet to be done: unit
tests, expanding abbreviations in statements and proof steps,
abbreviation introduction proof, abbreviation elimination proof.