First working version

Initial working version. More functionality is likely to be added,
mainly provability modulo theories, assertions and some form of
abstraction over formulae.