[plt-scheme] Expressing closures in PLT Redex

Say I have a language where closures are expressed as
environment-abstraction pairs:

(define lang
   (language
    (e-cxt hole (e-cxt E) (V e-cxt))

    (env ((var V) ...))

    (P (env E))

    (E V var (E E) #| and so on |#)

    (V ; values are numbers and closures
     number
     (lambda env (var) E))


So, for example, I might have a closure:

(lambda ((a 3) (b 4)) (x) (+ x a))

that adds 3 to its argument, and this closure happens to have captured b
as well.

Given that my programs, P are environment-expression pairs, what is the
best way to write the "AppLam" rule (in PLT Redex), that evaluates the
body of the closure in the closure's environment (appropriately
extended), and then resumes executing the context in its environment?

(reduction/name "AppLam" lang
    (env_1 (in-hole e-cxt_1 ((lambda env_2 (x) E_1) V_1)))
    << what goes here >>)

In << what goes here >>, I could have something along the lines of:

(in-hole e-cxt_1 (reduce (extended-env_2 E_1)))

However, that strikes me as a bit arbitrary.

Thanks.

Arjun