Use continuations for the backward functions

[sonmarcho]

The forward and backward functions lead to some duplication of code, which may lead to duplication in the proofs. A solution would be to make the forward functions return the backward functions as continuations. If we do so, we would also not need to filter the useless forward functions anymore.

It is unclear if doing this is really necessary, and if it would really be more practical to work on functions which return continuations rather than on the tuples (forward function, backward functions), but it is worth experimenting.

This may also make it more practical when working with functions which manipulate a state, when the backward function actually also updates the state (we will need to do so if we want to implement functions such as fn get_mut<T>(address : RawPointer<T>) -> &'a mut T).