Mutability translation with mutable cells

This PR introduces the Mutability Translation presented in my thesis.

Closes #157. Closes #140. Closes #99.

Summary The PR contains roughly these features/changes and all the refactoring/fixing that goes along:

Mutability is modelled with a mutable cell case class for all ADT fields and local variables:
```
case class MutCell[@mutable T](var t: T)
```
var and mutable flags are thus removed from the user-interface.
Mutable references are extracted and verified by means of the mutable cells.

This PR supersedes the two former mutability-related PRs #158 #159. It contains the grand majority of their changes though.

Two tests currently fail in the test suite, trait_bounds::verification and type_class::verification, due to the solver timing out, documented in this Stainless issue: https://github.com/epfl-lara/stainless/issues/1093.

epfl-lara / rust-stainless

Mutability translation with mutable cells #164