One subcase of method invocation.

Reorganized proof into sub-lemmas per case, to avoid timeouts. Still,
this case took a lot of fiddling to avoid timing out.