added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;

clarified future scheduling parameters, with support for parallel_limit;

misc tuning and clarification;

more tight treatment of subgoals: main goal may refer to extra variables;

optional proof context for unify operations, for the sake of proper local options;

clarified modules;