The design of \tgentzen{} makes the description of a
meta-interpreter easy:
\begin{ccprogram}
\agent tcc(\{C\})     :: \{C\}..
\agent tcc(C -> A)  :: C -> tcc(A)..
\agent tcc(C ~> A)  :: C ~> tcc(A)..
\agent tcc(next\ A)  :: next\  tcc(A)..
\agent tcc(Vars\$A)  :: Vars\$tcc(A)..
\agent tcc(Vars\Hat A)  :: Vars\Hat tcc(A)..
\agent tcc([])      :: []..
\agent tcc([A | B]) :: [tcc(A) | tcc(B)]..
\agent tcc(Proc)    :: Body\$((Proc::Body) -> tcc(Body)..
\end{ccprogram}

Only the last clause is interesting. Note that because of the way
sequences of clauses are interpreted in \tgentzen{}, the last
clause will be activated only on a agent that does not match any
of the other clauses. This can happen only for calls to
user-defined procedures. In such a case, the body of the
procedure is looked up, using a ``clause'' meta-call, and passed
on to a recursive invocation of the meta-interpreter.