#372 Proof by case on union membership

[Guillaume Verdier]

With an hypothesis like x∈S∪T, it is common to do a proof by case. This is currently done in two steps: first with “Remove membership” to obtain x∈S ∨ x∈T and then with “Proof by cases”. It would be faster if a tactic could do the proof by case directly on the first predicate.

[Laurent Voisin]

This can be implemented by creating a new level of the "Proof by cases" reasoner, and change the associated tactic in the GUI.

[Laurent Voisin]

Actually, we do not need to create a new level, because the new input of the reasone could not exist before. So we can just change the reasoner / tactic directly.

[Laurent Voisin]

Could also implement distinct case for a membership in an enumerated set,

[Guillaume Verdier]

These requests have been implemented and merged in commit [7ff1b1].