diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index 6f0be275e6e1b443f2f237e4c4f9817196b3a720..6f3f155c3904460fda7ddad836aa72ee83f12a2c 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -741,6 +741,7 @@ Proof.
   - right; eauto using reducible_no_obs_reducible.
 Qed.
 
+(** This is the top-level erasure theorem: erasure preserves adequacy. *)
 Theorem erasure e σ φ :
   adequate NotStuck e σ φ →
   adequate NotStuck (erase_expr e) (erase_state σ)