Provide for creating new derived rules

[cdibbs]

We should be able to define new rule justifications using:

1. A valid proof of the new rule
2. Special syntax for defining the justification format
3. (maybe) The ability to import such definitions from other files.

From the hip:

define justification MT n=1, m=2 <=> 6

p -> q : premise
~q : premise
| p
| q : -> elim 1,3

contradiction : not elim 2,4
~p : not intro 3-5