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