The effectful forcing technique allows one to show that the denotation of a closed System T term of type (ι→ι) →ι in the set-theoretical model is a continuous function (ℕ→ℕ) →ℕ. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees.