RHB Mutex example is wrong

[xldenis]

@fpoli pointed out that the mutex test case in Creusot is wrong. To be sound and faithful to RHB we should use a Mapping to hold our invariant (which we didn't have at the time).