Eval.hss

flatten-module
consider 'eval
ww-split [| wrap |] [| unwrap |]
{rhs-of 'work
   eta-expand 'e ; lam-body
   eta-expand 's ; lam-body
   eta-expand 'f ; lam-body
   unfold 'unwrap
   one-td (unfold 'f)
   bash
   {
     consider case ; [case-alt 1, alt-rhs] ; abstract 'm
     consider case ; [case-alt 1, alt-rhs] ; abstract 'n
   }
   any-bu (fold 'unwrap)
   any-bu (foreward (ww-fusion [| wrap |] [|unwrap|] [|work|]))
}
simplify
any-call (unfold 'wrap)