Lemmas should allow explicit code

We should have support for lemmas with explicit code in the hoare/prhoare triples/quadruples rather than just a path to a procedure.
This and applying such lemmas to possibly replace code would ease proof modularity