diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 23277892d937dd0f523ecf2efb51671981459862..62bb4a4c689b71ec3bcf25f3bd0016410e299e0a 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Export ectx_language ectxi_language.
+From iris.algebra Require Export cofe.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
 
@@ -508,6 +509,10 @@ Defined.
 
 Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
 Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
+
+Canonical Structure stateC := leibnizC state.
+Canonical Structure valC := leibnizC val.
+Canonical Structure exprC X := leibnizC (expr X).
 End heap_lang.
 
 (** Language *)