diff --git a/src/core/DY.Core.Trace.Base.fst b/src/core/DY.Core.Trace.Base.fst
index 9fcb23e..8f760bd 100644
--- a/src/core/DY.Core.Trace.Base.fst
+++ b/src/core/DY.Core.Trace.Base.fst
@@ -360,6 +360,10 @@ val find_event_triggered_at_timestamp_later:
     tr1 <$ tr2
   )
   (ensures find_event_triggered_at_timestamp tr1 prin tag content == find_event_triggered_at_timestamp tr2 prin tag content)
+  [SMTPat (find_event_triggered_at_timestamp tr1 prin tag content);
+   SMTPat (find_event_triggered_at_timestamp tr2 prin tag content);
+   SMTPat (tr1 <$ tr2)
+  ]
 let rec find_event_triggered_at_timestamp_later #label_t tr1 tr2 prin tag content =
   if length tr1 = length tr2 then ()
   else (
diff --git a/src/lib/event/DY.Lib.Event.Typed.fst b/src/lib/event/DY.Lib.Event.Typed.fst
index 9650a36..9db19f0 100644
--- a/src/lib/event/DY.Lib.Event.Typed.fst
+++ b/src/lib/event/DY.Lib.Event.Typed.fst
@@ -235,6 +235,10 @@ val find_event_triggered_at_timestamp_later:
     tr1 <$ tr2
   )
   (ensures find_event_triggered_at_timestamp tr1 prin content == find_event_triggered_at_timestamp tr2 prin content)
+  [SMTPat (find_event_triggered_at_timestamp tr1 prin content);
+   SMTPat (find_event_triggered_at_timestamp tr2 prin content);
+   SMTPat (tr1 <$ tr2)
+  ]
 let find_event_triggered_at_timestamp_later #a #ev_a tr1 tr2 prin content =
   reveal_opaque (`%find_event_triggered_at_timestamp) (find_event_triggered_at_timestamp #a);
   DY.Core.find_event_triggered_at_timestamp_later tr1 tr2 prin ev_a.tag (serialize a content)