Remove plainly_exist_1 from the BI axioms.
Added a PlainlyExist1BI
class for BIs that do have the property.
One slight annoyance is that this class has to appear in interface.v
. Otherwise, we have to add a dependency uPred.v
-> bi/derived.v
, which kill parallelism. Just tell me if you prefer this over the current alternative.
Edited by Robbert Krebbers