From 230b251b1032a9a342f41a1097139b0ba8c5c3ae Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Mon, 6 Apr 2026 11:09:13 -0400 Subject: [PATCH] remove stray printing of lemma --- theories/modules/EventPartitioning.ec | 1 - 1 file changed, 1 deletion(-) diff --git a/theories/modules/EventPartitioning.ec b/theories/modules/EventPartitioning.ec index 479a79fac0..4939f847eb 100644 --- a/theories/modules/EventPartitioning.ec +++ b/theories/modules/EventPartitioning.ec @@ -128,7 +128,6 @@ theory ResultPartitioning. = big predT (fun a=> Pr[M.f(i) @ &m: E i (glob M) res /\ res = a]) (undup (X i)) + Pr[M.f(i) @ &m: E i (glob M) res /\ !mem (X i) res]. proof. -print mem_undup. have->:Pr[M.f(i) @ &m : E i (glob M){hr} res{hr} /\ ! (res{hr} \in X i)]= Pr[M.f(i) @ &m : E i (glob M){hr} res{hr} /\ ! (res{hr} \in undup (X i))]. - smt(mem_undup).