Unify spec encoding for impl & fns

[yannbolliger]

Specs can't be added to trait implementation functions at the current time.

Therefore, we want to move forward by encoding them as closures inside the actual function and hence unify the way we encode specs in implementation blocks and all other (non-abstract) functions. This is also similar to what Prusti is doing.

Cool things
While Stainless doesn't play along super-well for some proofs that use measures, it is nice to see that #[law] refinement in implementations of traits works out of the box. 🚀

Limitations
While the current approach solves the problems of specs in trait implementations, it's still impossible to add specs to the abstract methods in traits.

Further questions:

• Can we annotate lambdas/expressions in a code block?
• From @romac: Think about how to encode specs for abstract trait members (ie. might need to give the abstract members a body in order to express the specs)
• Remove --infer-measures=no --check-measures=false and turn on/comment in all the measure specs.
• Do we want to run the contracts, left open.

The follow-up work to solve the problem for traits is tracked here: #85. Measure inference: #86.