Re: double switch

Observe, that rule s is just the special case of s' with E=f.  The
derivation you were looking for becomes

      ([R,U],T)
=   -------------
    ([R,U],[T,f])
s'  --------------
    [(R,T),[U,f]]
=   --------------
      [(R,T),U]



--Robert