`wp_apply` cannot deal with curried lemmas
The 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.