Comment by justosophy

See the Coq proofs in https://github.com/barry-jay-personal/tree-calculus/ for the pre-typed tree content as well.