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