diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 9989f8a6c7f425f0cc0b00da690ca4586984c637..26459e9ad6c4507f3a1c0391325442385bc87899 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].