I've had a similar problem, there is nothing that useful I'm afraid. Probably best to look into general discussions of trees.

One thing worth trying to do (if you can) is separate the generation of the tree from the tree itself -- hopefully you can imagine the tree existing as a complete object (even though you never store it all), and formulate proofs based on that.