Fix fuel issue for mutually recursive functions in the interpreter

[sonmarcho]

In the current encoding of the proof obligations sent to Boogie, unfolding any function in a group of mutually recursive function consumes fuel. Because this lead to difficulties when doing the proofs, we inlined all the definitions like InterpBlock, InterpBind, etc. in the InterpExpr function, so that in the Block, Bind, etc. cases we don't need to consume two units of fuel (one for InterpExpr, then one for InterpBlock, ...) to reveal what the interpreter actually does. As a consequence, the InterpExpr function has become big: this should be fixed.