From ec0816bff58da86c387c3f6a1bc0a134e2e8d849 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Nov 2017 17:15:28 +0100
Subject: [PATCH] Carry `saved_anything_agree` out in the proof mode.

It does not really help since the main work of the proof is in showing that
`cFunctor_map F (iProp_fold, iProp_unfold)` is injective, but whatever.
---
 theories/base_logic/lib/saved_prop.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 8d9939d90..c07150d1f 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -42,15 +42,15 @@ Section saved_anything.
   Lemma saved_anything_agree γ x y :
     saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y.
   Proof.
-    (* TODO: Use the proof mode. *)
-    apply wand_intro_r.
-    rewrite -own_op own_valid agree_validI agree_equivI.
+    iIntros "Hx Hy". rewrite /saved_anything_own.
+    iDestruct (own_valid_2 with "Hx Hy") as "Hv".
+    rewrite agree_validI agree_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. apply f_equiv, _.
+    rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
   Qed.
 End saved_anything.
 
-- 
GitLab