Support the kind of change Reviewer 2 was interested in

[tlringer]

R2: I personally would be interested in dealing with the correspondence between trees and terms easily (in CoLoR for Coq terms are implemented using dependent types (number of arguments equal to the arity of the symbol); in Isafor for Isabelle they are implemented as rose trees (formally: using varyadic symbols), but i failed to make that work: (Error: Anomaly "Uncaught exception Failure("this kind of change is not yet supported")." Please report at http://coq.inria.fr/bugs/.) Will that be covered by future work?

It's kind of hard to know what R2 wants without seeing the type examples explicitly, but I should look into this at some point.

Also, I fixed this to not be an anomaly already, and to tell people to post issues here so I can ask them for their types.

[tlringer]

Try with the new framework