`wp_apply` cannot deal with curried lemmas
wp_apply tactic was written in a time when all our lemmas were uncurried. It always distributes all the resources of the current context to one of the goals that it creates, not leaving any control to the user. I think we need something like
wp_apply with "<spec pattern>" to accommodate curried lemmas.
See https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf/theories/lang/spawn.v#L77 and https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/6d36b8cfbe2e7dbeda13889b17ef4b168d6953cf/theories/typing/unsafe/cell.v#L165 for some examples.