Handle probabilities in the core

Should they be handled manually or automatically like the base FreeSpec would ?

Currently have this to prove :
```rocq
match proj_p (inj_p (CanWork p)) with
| Some e => doors_o_caller ω bool e
| None => True
end
```

which is not a trivial goal