diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index ff8d2bb4ba83282714ae08c57916734683facca8..9fe2981cb7d4c0e4ab537f724a5bdb5ddaf1c8d9 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -28,6 +28,8 @@ Section type_soundness.
 
   Definition main_transformer : predl_trans'ₛ [] () := (λ post '-[], post ()).
 
+  (* Intuitively, it says that execution of a closed, semantically well-typed
+    program, without any special precondition, does not get stuck *)
   Theorem type_soundness `{!typePreG Σ} (main : val) σ t :
     (∀ `{!typeG Σ}, typed_val main main_type main_transformer) →
     rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →