-
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