diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 0d000fe3fc075252d9da11e2d21b1b371ddfc7e6..71c8b53d66631e9c42a189c1ba160cc3a69dbf85 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -484,3 +484,8 @@ Tactic Notation "wp_select" "with" constr(pat) :=
   end.
 
 Tactic Notation "wp_select" := wp_select with "[//]".
+
+Tactic Notation "wp_new_chan" constr(prot) "as"
+       "(" simple_intropattern(c1) simple_intropattern(c2) ")" constr(pat) :=
+  wp_smart_apply (new_chan_spec prot); [done|];
+  iIntros (c1); iIntros (c2); iIntros pat.