697.lean:24:12-24:19: error: invalid use of `partial`, `pregion` is not a function
  P Unit