Added constructors to the context and fixed the proving the theorem twice bug.