derived actions

[ivoysey]

we need a good description of a way to give a proof of admissibility of a new action in terms of the existing ones; i guess that amounts to macros?

[ivoysey]

from the old todo file:

- a richer notion of actions that allows for derived action forms. so if
  you can prove that a new action you have is admissible with respect to
  existing ones, you should be able to use it freely without needing to
  change the core proofs. like prevsib from the TFP work can be expressed
  with nextsib, parent, and first child.

[ivoysey]

migrating this to the issue tracker repo.