fupd_proper is too weak
The type should be
Global Instance fupd_proper:
forall (PROP : sbi) (H : BiFUpd PROP),
Proper (equiv ==> equiv ==> equiv ==> equiv) (@fupd (sbi_car PROP) _).
Proof using.
Admitted.
The type should be
Global Instance fupd_proper:
forall (PROP : sbi) (H : BiFUpd PROP),
Proper (equiv ==> equiv ==> equiv ==> equiv) (@fupd (sbi_car PROP) _).
Proof using.
Admitted.