let sigma op al =
  match op, al with
    | Apply(r), x :: xl -> 
        mk_apply mk_app r x xl   (* no simplifications *)
    | Abs, [x] -> 
        mk_abs x
    | _ -> 
        assert false