removed short ?abbreviations; combined several easy proof steps; split assumptions into atomic ones
improved documentation of partition_without; done cleaning up indstep
* better readability
* higher performance (fewer steps, better invocation of built-in automated provers)