From 398e682ff2d936d1fcb30b2a8c4423eeadcc4903 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20=C3=85man=20Pohjola?= Date: Tue, 5 Sep 2023 13:27:36 +1000 Subject: [PATCH] Fix a shadowed lemma name --- src/coalgebras/itreeTauScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml index bdcdcb20fe..a4fe6414b7 100644 --- a/src/coalgebras/itreeTauScript.sml +++ b/src/coalgebras/itreeTauScript.sml @@ -787,7 +787,7 @@ Proof metis_tac[strip_tau_rules,itree_wbisim_rules] QED -Theorem itree_wbisim_tau: +Theorem itree_wbisim_tau_eq: itree_wbisim (Tau t) t Proof ‘!t t'. t = Tau t' \/ t = t' ==> itree_wbisim t t'’ suffices_by metis_tac[] \\