diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index a8b975d481a95df4b24f2f1f2ae63e9294aa9618..e1585242f58a882222d2b342dd582c94347e085c 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -465,7 +465,7 @@ Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: sta
   {| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
 Arguments state_upd_used_proph_id _ !_ /.
 
-Inductive head_step : expr → state → list observation → expr → state → list (expr) → Prop :=
+Inductive head_step : expr → state → list observation → expr → state → list expr → Prop :=
   | RecS f x e σ :
      head_step (Rec f x e) σ [] (Val $ RecV f x e) σ []
   | PairS v1 v2 σ :