split_vc breaks splitting of "[@case_split]" conditions
split_goal_right + split_goal_right works correctly: first it splits the goal on the right, then the [@case_split] premises.
split_vc + split_vc does not work because of introduce_premises. This makes split_vc pretty much incompatible with SP (aka fast WP) which relies heavily on [@case_split].
Possible solutions:
- make split_goal_right work on local premises (generated by introduce_premises)
- make split_vc use a special variant of split_goal_right that works on local premises
- make split_vc reassemble the local premises before splitting them with split_goal_right