Commit 88e0b05b authored by Robbert Krebbers's avatar Robbert Krebbers

Internalize equality property for agree.

parent 399cb6ef
......@@ -131,6 +131,8 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
(** Internalized properties *)
Lemma agree_equivI {M} a b : (to_agree a to_agree b)%I (a b : uPred M)%I.
Proof. split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne. Qed.
Lemma agree_validI {M} x y : (x y) (x y : uPred M).
Proof. by intros r n _ ?; apply: agree_op_inv. Qed.
End agree.
......
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