From cbf81b65f8f11685369a93ab6ed91e7f56c94346 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Oct 2020 02:12:32 +0200
Subject: [PATCH] Add lemma `cmra_transport_trans`.
---
theories/algebra/cmra.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index de26c43e8..df45c6aaf 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -959,6 +959,10 @@ Proof. rewrite /urFunctorContractive; apply _. Qed.
Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
eq_rect A id x _ H.
+Lemma cmra_transport_trans {A B C : cmraT} (H1 : A = B) (H2 : B = C) x :
+ cmra_transport H2 (cmra_transport H1 x) = cmra_transport (eq_trans H1 H2) x.
+Proof. by destruct H2. Qed.
+
Section cmra_transport.
Context {A B : cmraT} (H : A = B).
Notation T := (cmra_transport H).
--
GitLab