Improve handling of premises
- Add a meta on top of the toplevel goals (
split_theory
? IDE?) for display purpose. - Systematically add a transformation node that performs
split
andintro
on a VC (can be disabled by a configuration option). - Modify
split_goal
so that it splits the last labeled disjunction in the context. - Remove the implicit
introduce_premises
used for display purpose.