diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index a30b5a7d6edc7833cf2d26cccf4d245f7bee0f65..1e051b4861733dc3e483cf64aee5028e512b496a 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -324,3 +324,5 @@ Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
   let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Λ in
   @Language E V St K of_val to_val _
     (@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).
+
+Global Arguments LanguageOfEctx : simpl never.
diff --git a/iris/program_logic/ectxi_language.v b/iris/program_logic/ectxi_language.v
index 55dc11ff86a7cef2ba7e0a97000a0513df372c68..0f083de0a465273f59c5e6a69912e1e8e78bc1ad 100644
--- a/iris/program_logic/ectxi_language.v
+++ b/iris/program_logic/ectxi_language.v
@@ -164,3 +164,5 @@ Definition EctxLanguageOfEctxi (Λ : ectxiLanguage) : ectxLanguage :=
   let '@EctxiLanguage E V C St K of_val to_val fill head mix := Λ in
   @EctxLanguage E V (list C) St K of_val to_val _ _ _ _
     (@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St K of_val to_val fill head mix)).
+
+Global Arguments EctxLanguageOfEctxi : simpl never.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 67af46d8f2fc6584105128398bff68f383069fe5..2c9207a87581dd4baa63467d40d87730fa22a6ed 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -165,6 +165,20 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   --------------------------------------∗
   |={⊤}=> True
+"test_heaplang_not_unfolded"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  ============================
+  @bi_emp_valid (uPredI (iResUR Σ))
+    (@fupd (bi_car (uPredI (iResUR Σ)))
+       (@bi_fupd_fupd (uPredI (iResUR Σ))
+          (@uPred_bi_fupd Σ
+             (@iris_invGS heap_lang Σ (@heapGS_irisGS Σ heapGS0))))
+       (@top coPset coPset_top) (@top coPset coPset_top)
+       (@bi_pure (uPredI (iResUR Σ)) True))
 1 goal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 0e80ada63a78541a97c6b73c5e050b5486fd5cc2..c20fdf92b1a3259b1093f8788d014782ee288130 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -326,6 +326,16 @@ Section tests.
   Proof.
     wp_pures. Show. (* No second fupd was added. *)
   Abort.
+
+  Check "test_heaplang_not_unfolded".
+  Lemma test_heaplang_not_unfolded :
+    ⊢@{iPropI Σ} |={⊤}=> True.
+  Proof.
+    cbn.
+    Set Printing All.
+    Show.
+    Unset Printing All.
+  Abort.
 End tests.
 
 Section mapsto_tests.