Do not accept a step selection if a site selection is (also) needed.
Back out more aggressive use of left elision, but still be somewhat more aggressive.
Describe considerPart like consider.
Make the rule selector widget fade away while a rule is running.
Modify rules.regroupAdditions to produce more readable proofs.