Improve case transformation
It is my feeling that VC generation/split often produces hypotheses containing implications with the same premises (or its negation) such as:
H: P -> A
H1: not P -> B
H2: P -> C
On these cases, I think the user would like case P
to remove unsatisfiable hypothesis and premises. This would give two new context:
H: A
H2: C
H3: P
and
H1: B
H: not P