Working proof system with interpretations.
Added some TODO comments to code.