It not behaves more consistently with iExact and thus also works in the
case H : P -★ □^n Q |- Q.