Elimination rules for datatypes look like this:

In a refinement proof we exploit our ability to choose \Phi to attack 'the goal at hand'. \Phi abstracts the motive for the elimination. The subgoals so generated not only expose the 'predecessors' of the x's, they also yield more specific applications of \Phi, rewriting the goal in the light of the new information available. Such rules explain the leverage that the assumptions listed in the x's give us on an arbitrary goal.

I give a tactic to apply rules in this style, and I use this tactic not only with the native rules supplied with datatypes and relations, but also with derived rules of the above form. The tactic takes any such theorem (suitably annotated) and turns it into a left rule in the sense of the sequent calculus. Examples of such rules are used to