From 5481ecc536eac44d2fe727e1306d6d80651cb20f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jan 2016 17:23:17 +0100
Subject: [PATCH] Inverse lemma of to_agree.

---
 modures/agree.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/modures/agree.v b/modures/agree.v
index 173c81977..212be59d3 100644
--- a/modures/agree.v
+++ b/modures/agree.v
@@ -133,6 +133,8 @@ Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
 Global Instance to_agree_inj n : Injective (dist n) (dist n) (to_agree).
 Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
+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.
 End agree.
 
 Arguments agreeC : clear implicits.
-- 
GitLab