• Robbert Krebbers's avatar
    Remove FIXME. · a095bb8a
    Robbert Krebbers authored
    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)'.
    a095bb8a
counter_examples.v 2.31 KB