better parsing for "show" and "have" structured proof branch completions
simplified "have" command handling - using a lookahead;

This means that "have" itself introduces an assumption in analysis, without waiting for the finishing command..
cleanup type
more consistent `by` handling
basic handling for "fix"
special handling for `proof -`
trim command text