[plt-scheme] (Off) Tool for Visualizing Beta-Reductions?

Hi,

Sorry for this slightly off-topic question. I'm working in intensional
natural language semantics (aka "Montague Grammar"), where the lexical
meaning of expressions is sometimes (not always) specified in ordinary
language, like in this example where the expression type is given as a
subscript:

(\lambda x_e. x_e walks) john_e

==> john_e walks

Now imagine rather complicated formulas with complex functional types
and lots of function applications. Think of generalized quantifiers
being modified by prepositions to yield sentence- to sentence-type
operators and fancy stuff like that. It turns out to be very cumbersome
and error-prone to do all the beta-reductions by hand that come up in
examples.

Does anyone know a tool that visualizes individual reduction steps, but
also allows for the inclusion of arbitrary strings like "walks" in the
above trivial example? Can the PLT redex tool be used for this?

Best regards,

Erich