Skip to content

Add derived ≼ connective on the BI level.

Ike Mulder requested to merge snyke7/iris:ike/internal_included into master

For !930 it was useful to have the connective on the BI level.

I originally defined it for uPreds, but since it has seen usage for non-uPred bis, I have generalized it.
Current location is at bi/lib/cmra.v.

This MR is turning out to be a bit larger than I expected, after I started moving all useful lemmas from !930 on here. It currently contains the following changes:

  • Defining the connective, proofmode support for it, and some useful lemmas
  • Moving some lemmas on excl and csum that were stated for uPreds, but provable for general bis with .
  • Add two additional hints for on the Prop level, which makes eauto more useful.
Edited by Ike Mulder

Merge request reports