diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 2005837fbb3ebf5df3f245df14dcdbd665a61eae..dfda68af9222fe27d304c7648150996369c2720c 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -135,7 +135,7 @@ Section classes.
     (∀.. x1, MsgTele (tele_app tm1 x1) tv2 tP2 (tele_app tp x1)) →
     ProtoNormalize d (<a> m) pas (<!.. x2> MSG tele_app tv2 x2 {{ tele_app tP2 x2 }};
                                   <?.. x1> MSG tele_app tv1 x1 {{ tele_app tP1 x1 }};
-                                  tele_app (tele_app tp x1) x2).
+                                  tele_app (tele_app tp x1) x2) | 1.
   Proof.
     rewrite /ActionDualIf /MsgNormalize /ProtoNormalize /MsgTele.
     rewrite tforall_forall=> Ha Hm Hm' Hm''.