From 0797ced71d4b2a9bcd04069bf981b88ff31311c0 Mon Sep 17 00:00:00 2001
From: wkolowski <wkolowski@protonmail.com>
Date: Wed, 13 Dec 2023 16:15:26 +0100
Subject: [PATCH] Code review.

---
 theories/Core/Equivocation/TraceWiseEquivocation.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Core/Equivocation/TraceWiseEquivocation.v b/theories/Core/Equivocation/TraceWiseEquivocation.v
index f8739fce..f991f198 100644
--- a/theories/Core/Equivocation/TraceWiseEquivocation.v
+++ b/theories/Core/Equivocation/TraceWiseEquivocation.v
@@ -95,7 +95,7 @@ Lemma elem_of_equivocating_senders_in_trace
   : v ∈ equivocating_senders_in_trace tr <->
     exists (m : message),
     (sender m = Some v) /\
-    equivocation_in_trace (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) m tr.
+    equivocation_in_trace (free_composite_vlsm IM) m tr.
 Proof.
   unfold equivocating_senders_in_trace.
   rewrite elem_of_remove_dups, elem_of_list_omap.