From 206fa666f4dd8500055385e81ff83d93b1d8143c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 3 Dec 2018 14:50:25 +0100
Subject: [PATCH] Prove `agree_map f (to_agree x) = to_agree (f x)`.

---
 theories/algebra/agree.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 1f6404d4b..5c13b21c9 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -255,6 +255,9 @@ Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed.
 Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
   agree_map (g ∘ f) x = agree_map g (agree_map f x).
 Proof. apply agree_eq. by rewrite /= list_fmap_compose. Qed.
+Lemma agree_map_to_agree {A B} (f : A → B) (x : A) :
+  agree_map f (to_agree x) = to_agree (f x).
+Proof. by apply agree_eq. Qed.
 
 Section agree_map.
   Context {A B : ofeT} (f : A → B) `{Hf: NonExpansive f}.
-- 
GitLab