diff --git a/include/lemmas.spthy b/include/lemmas.spthy
index 69b4025d32d076efbc0ca2aaedca9c620fd568a9..4335d5dba874026401b61ab43ac76aeb2ae1b969 100644
--- a/include/lemmas.spthy
+++ b/include/lemmas.spthy
@@ -99,6 +99,7 @@ lemma key_secrecy:
     ==> not(Ex #m . K(k) @ #m)
         | (Ex #m . Revealed(sid) @ #m)
         | (Ex #m . Corrupted(C) @ #m)
+        | (Ex #m . Corrupted(T) @ #m)
   "
 
 // Cannot track chip before CA