Some fixes to proving implications.
More on improvement.

Currently, there's a bug, where types seem to be going negative!