diff --git a/verify.saw b/verify.saw
index e541c6c..5e6abe1 100644
--- a/verify.saw
+++ b/verify.saw
@@ -5,8 +5,10 @@ for [0,1,2,16,63,64,65,127,128,129,255,256] (\p -> do {
     print ("decrypt_encrypt",a,p);
     prove_print (unint_yices ["Ascon::Ascon_p"]) {{
         \K N (A : [a]) (P : [p]) ->
-        case AEAD128_decrypt K N A (AEAD128_encrypt K N A P) of
-            None -> False
-            Some p' -> p' == P
+            (case AEAD128_decrypt K N A C T of
+                None -> False
+                Some p' -> p' == P
+            where
+            (C,T) = AEAD128_encrypt K N A P)
     }};
 }));