purityTT.v: A proof for the case of parametricity in Tree monad is added.
Other minor changes.