diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index f752401f2ae4c60a2cd22257d30022ed24f659e4..2020e1933034a167edc33bf812f49ff43755f9f7 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -67,7 +67,7 @@ Section typing.
 
   (* Same for the other direction *)
   Lemma tctx_unmk_cell E L ty p :
-    tctx_incl E L [p ◁ ty] [p ◁ cell ty].
+    tctx_incl E L [p ◁ cell ty] [p ◁ ty].
   Proof.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.