- split_* splits on the right-hand side
- full_split_* splits on the both sides
- split functions do not propagate labels
- remove split_conjunction, subsumed by split_goal