added local annotation to iter_resp_wbisim ret tau case

HOL-Theorem-Prover · Oct 9, 2023 · 5923911 · 5923911
1 parent 9c6512c
commit 5923911
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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))