Update the case tactic for backchaining sequents

Previously it would always produce a member assumption.
Now it eagerly traverses the context and makes new cases for every
element of the context.
This might break existing proofs. To be tested.