1.) iDestruct is able turns  into two implications (because uPred_iff
    is (type classes) transparent).
2.) iApply only backtracks on turning P  Q into P → Q or Q → P when
    there are no future premises. This is not the case for
    'P  □ (P → False)'.