Commit edae2dc1 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Lemma -> Global Instance.

parent d4c6321c
......@@ -610,7 +610,7 @@ Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_pro
(** PlainlyExist1BI *)
Lemma uPred_plainly_exist_1 : PlainlyExist1BI (uPredI M).
Global Instance uPred_plainly_exist_1 : PlainlyExist1BI (uPredI M).
Proof. unfold PlainlyExist1BI. by unseal. Qed.
(** Limits *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment