testb handles the test in [?Q]P by assuming the test succeeds with an implication Q→P, because test ?Q can only make a transition when formula Q holds true.

Other tactics such as chase and unfold also use this axiom.