diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml
index 978845ceba..3f9bd8e7c5 100644
--- a/src/coalgebras/itreeTauScript.sml
+++ b/src/coalgebras/itreeTauScript.sml
@@ -1038,7 +1038,7 @@ Proof
   metis_tac[itree_bind_resp_t_wbisim, itree_bind_resp_k_wbisim, itree_wbisim_trans]
 QED
 
-Theorem itree_iter_ret_tau_wbisim:
+Theorem itree_iter_ret_tau_wbisim[local]:
   itcb1 = (λx. case x of INL a => Tau (itree_iter k1 a) | INR b => Ret b) /\
   itcb2 = (λx. case x of INL a => Tau (itree_iter k2 a) | INR b => Ret b) /\
   itree_wbisim (Ret x) (Tau u) /\ (!r. itree_wbisim (k1 r) (k2 r))