diff --git a/iris_core.v b/iris_core.v
index 5609f3f4484f0d58ffeec7eab6ab0e560b3677bb..b6835b6b4eb983e988550af32874009ba01799d7 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -189,6 +189,19 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
   
   End Timeless.
 
+  Section IntEqTimeless.
+    Context {T} `{tT: Setoid T}.
+    (* This only works for types with the discrete metric! *)
+    Local Instance mT: metric T := discreteMetric.
+
+    Lemma intEqTimeless (t1 t2: T):
+      valid(timeless(intEq t1 t2)).
+    Proof.
+      intros w n r. intros w' k r' Hsq Hlt.
+      simpl. tauto.
+    Qed.
+  End IntEqTimeless.
+
   Section Ownership.
 
     (** Ownership **)