flatten-module
consider 'last
{consider 'last
  load "../WWSplitTactic.hss"
  {rhs-of 'work
     eta-expand 'b
     0
     eta-expand 'bs
     0
     unfold 'unwrap
     unfold 'f
     case-reduce
     consider app
     unfold 'wrap
     case-reduce
  }
}
simplify
any-call (unfold 'wrap)