diff --git a/program_logic/model.v b/program_logic/model.v
index ce2cf3f1b62ad2a9ac3bec02ac7447fc20f4f0ed..08960cef5dd54e6ff70ee616cb06497314f1c873 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,5 +1,8 @@
 From iris.algebra Require Export upred.
 From iris.program_logic Require Export resources.
+(* We'd prefer to only import this in the sealed module, to make sure it does
+   not "escape". However, for some reason, that breaks importing model.v
+   elsewhere. *)
 From iris.algebra Require Import cofe_solver.
 
 (* The Iris program logic is parametrized by a locally contractive functor