Export derivation to tikz depends on current state

[akissinger]

This behaviour has confused me on multiple occasions. I think better would be to:

1. refuse to export if there are no non-trivial proof heads
2. if there is a unique proof head, export ROOT => HEAD
3. if there are multiple proof heads, warn: There are multiple proof heads, this will export latex up to step "foo", and give chance to cancel.