Syntax assigned to tactic is incorrect

[antonkov]

For example for cases the syntax to the cases tactic is everything with all insides, but we split by \n and therefore we display only
cases h with rw[hep].

Instead we should assign "the remaining" syntax, i.e.g only cases h with since rw[hep] is consumed by tactic.

Or maybe it should be generated by completely different algorithm. Syntax assignment heuristic works ok-ish but definitely not always correct