diff --git a/src/nagini_translation/resources/tuple.sil b/src/nagini_translation/resources/tuple.sil
index 6ba49594..4637b477 100644
--- a/src/nagini_translation/resources/tuple.sil
+++ b/src/nagini_translation/resources/tuple.sil
@@ -133,6 +133,24 @@ function tuple___eq__(self: Ref, other: Ref): Bool
                                { tuple___getitem__(other, i)}
                                i >= 0 && i < tuple___len__(self)
                                 ==> object___eq__(tuple___getitem__(self, i), tuple___getitem__(other, i))))
+    ensures result <==>
+            (tuple___len__(self) == tuple___len__(other) &&
+             (forall i: Int :: { tuple___getitem__(self, i) }
+                               { tuple___getitem__(other, i)}
+                               i <= -1 && i >= -tuple___len__(self)
+                                ==> object___eq__(tuple___getitem__(self, i), tuple___getitem__(other, i))))
+    ensures result <==>
+            (tuple___len__(self) == tuple___len__(other) &&
+             (forall i: Ref :: { tuple___getitem__(self, int___unbox__(i)) }
+                               { tuple___getitem__(other, int___unbox__(i))}
+                               issubtype(typeof(i), int()) && int___unbox__(i) >= 0 && int___unbox__(i) < tuple___len__(self)
+                                ==> object___eq__(tuple___getitem__(self, int___unbox__(i)), tuple___getitem__(other, int___unbox__(i)))))
+    ensures result <==>
+            (tuple___len__(self) == tuple___len__(other) &&
+             (forall i: Ref :: { tuple___getitem__(self, int___unbox__(i)) }
+                               { tuple___getitem__(other, int___unbox__(i))}
+                               issubtype(typeof(i), int()) && int___unbox__(i) <= -1 && int___unbox__(i) >= -tuple___len__(self)
+                                ==> object___eq__(tuple___getitem__(self, int___unbox__(i)), tuple___getitem__(other, int___unbox__(i)))))
 
 
 domain tuple_types {