From 4e7e85790424325ae2e6713b3ae9fe3a0db7ddeb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2016 02:35:40 +0100
Subject: [PATCH] Add lemma Shot_core.

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

diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 9989f8a6c..26459e9ad 100644
--- a/algebra/one_shot.v
+++ b/algebra/one_shot.v
@@ -158,6 +158,9 @@ Instance one_shot_op : Op (one_shot A) := λ x y,
 
 Lemma Shot_op a b : Shot a â‹… Shot b = Shot (a â‹… b).
 Proof. done. Qed.
+Lemma Shot_core a : core (Shot a) = Shot (core a).
+Proof. done. Qed.
+
 Lemma Shot_incl a b : Shot a ≼ Shot b ↔ a ≼ b.
 Proof.
   split; intros [c H].
-- 
GitLab