A non-ssreflect way of proceeding here is to simply destruct (boolP bar) as x. I would presume that the ssreflect-case tactic is buggy here but do not know enough about ssreflect to be certain.