 To see that a dynamic higher order system is expressible in ITL, it is enough to show how to define the appropriate dynamic operations. Assume \(\phi\) and \(\psi\) have the type of context transitions, i.e. type [\(e] \rightarrow[e] \rightarrow t\) (using [\(e\)] for arbitrary contexts), and that \(c, c', c''\) have type [\(e\)]. Then we can define the dynamic existential quantifier, dynamic negation and dynamic composition as follows: 