Generalize the type of gmap_equivI.

parent d76f0a7f
...@@ -94,6 +94,9 @@ Global Instance gmap_singleton_discrete i x : ...@@ -94,6 +94,9 @@ Global Instance gmap_singleton_discrete i x :
Lemma insert_idN n m i x : Lemma insert_idN n m i x :
m !! i {n} Some x <[i:=x]>m {n} m. m !! i {n} Some x <[i:=x]>m {n} m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed. Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
Lemma gmap_equivI {M} m1 m2 : m1 m2 @{uPredI M} i, m1 !! i m2 !! i.
Proof. by uPred.unseal. Qed.
End cofe. End cofe.
Arguments gmapO _ {_ _} _. Arguments gmapO _ {_ _} _.
...@@ -232,8 +235,6 @@ Qed. ...@@ -232,8 +235,6 @@ Qed.
Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin. Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
(** Internalized properties *) (** Internalized properties *)
Lemma gmap_equivI {M} m1 m2 : m1 m2 @{uPredI M} i, m1 !! i m2 !! i.
Proof. by uPred.unseal. Qed.
Lemma gmap_validI {M} m : m @{uPredI M} i, (m !! i). Lemma gmap_validI {M} m : m @{uPredI M} i, (m !! i).
Proof. by uPred.unseal. Qed. Proof. by uPred.unseal. Qed.
End cmra. End cmra.
......
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