Documentation

Solve class constraints. If not, then we return Nothing. If solved, ther we return Just a list of sub-goals.

Add propositions that are implied by the given one. The result contains the orignal proposition, and maybe some more.