[racket] Transitively extend redex metafunctions

The various extension forms for redex are critical for code re-use, but 
extensions break down when the things (metafunctions, judgments, etc.) 
being extended are not monolithic, but instead call helper metafunctions 
or judgments.  Due to the paucity of binding forms for these things, 
sometimes separate helper metafunctions are unavoidable (e.g. if you 
write an accumulator-style metafunction, you will need two top-level 
definitions; you can't place the metafunction with the accumulator 
within the definition of the other).

Here is an example that demonstrates the problem.  First a good use of 
extension:

(define-language L
   (A string))

(define-metafunction L
   f : any -> #t or #f
   [(f A) #t]
   [(f any) #f])

(define-extended-language M L
   (A .... number))

(define-metafunction/extension f M
   g : any -> #t or #f)

(test-equal (term (g "x")) #t)
(test-equal (term (g 7))   #t) ;; as we'd expect since 7 is an A in M

Now, let's define two seemingly equivalent metafunctions, but have a 
call to a *helper* metafunction, in this case f:

(define-metafunction L
   h : any -> #t or #f
   [(h A) (f A)]
   [(h any) #f])

(define-metafunction/extension h M
   i : any -> #t or #f)

(test-equal (term (i "x")) #t)
(test-equal (term (i 7))   #t) ;; this fails since 7 is not an A in *L*

Here the call to i re-interprets h on language M, but the call to f does 
no re-interpretation, so its using f as a metafunction of langauge L 
causing the test to fail.

It seems like the right thing is to transitively re-interpret all 
metafunctions and judgments that are *used* when extending a 
metafunction or judgment.

If this kind of general solution can't be supported, what would go a 
long way for me is to have the ability to locally bind helper 
metafunctions within a metafunction definition and have those be 
re-interpreted when the metafunction is re-interpreted.

In other words, I'd be happy if I could write this and have it work:

(define-metafunction L
   h : any -> #t or #f
   [(h A) (f A)]
   [(h any) #f]
   with
   f : any -> #t or #f
   [(f A) #t]
   [(f any) #f])

(define-metafunction/extension h M
   i : any -> #t or #f)

David