diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 9bd73963486768785bf088d3c356f562d6a43fda..b9c109be9543f59b4cadc761b9d754e725ca3f4a 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -7,7 +7,7 @@ From lrust.typing Require Import type lft_contexts type_context.
 Section cont_context_def.
   Context `{typeG Σ}.
 
-  Definition cont_postcondition : iProp Σ := False%I.
+  Definition cont_postcondition : iProp Σ := True%I.
 
   Record cctx_elt : Type :=
     CCtx_iscont { cctxe_k : val; cctxe_L : llctx;