cleanup

REPROSEC · Oct 22, 2024 · d4eac52 · d4eac52
1 parent 40aad89
commit d4eac52
Showing 1 changed file with 4 additions and 6 deletions.
diff --git a/src/core/DY.Core.Trace.Manipulation.fst b/src/core/DY.Core.Trace.Manipulation.fst
@@ -538,12 +538,10 @@ val get_state_state_was_set:
   Lemma
   (ensures (
     let (opt_content, tr_out) = get_state prin sess_id tr in
-    tr == tr_out /\ (
-      match opt_content with
-      | None -> True
-      | Some content -> 
-          state_was_set tr prin sess_id content
-    )
+    match opt_content with
+    | None -> True
+    | Some content ->
+        state_was_set tr prin sess_id content
   ))
   [SMTPat (get_state prin sess_id tr)]
 let get_state_state_was_set prin sess_id tr =