refined the b-causality rule for CheckWithin (in accordance with the Coq formalisation)