diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec
index 518a00c5dd..ef97e5a137 100644
--- a/examples/ChaChaPoly/chacha_poly.ec
+++ b/examples/ChaChaPoly/chacha_poly.ec
@@ -1467,7 +1467,7 @@ section PROOFS.
                Mem.log{1} Mem.log{2} Mem.lc{1} Mem.lc{2} 
                BNR.lenc{1} BNR.lenc{2} BNR.ndec{1} BNR.ndec{2} /\
            check_plaintext BNR.lenc{1} p{1} ).
-      + by ecall (equ_cc n{1} ROin.m{1} ROout.m{1}); rewrite /check_plaintext; auto => /> /#.
+      + ecall (equ_cc n{1} ROin.m{1} ROout.m{1}); auto => /> /#.
       move=> {&m};inline{1} 5; inline{1} 8.
       rcondt{1} ^if.
       + move=> &m; auto => />; rewrite /SplitD.test /= C.insubdK //=.
@@ -1644,7 +1644,7 @@ section PROOFS.
                   BNR.lenc{1} BNR.lenc{2} BNR.ndec{1} BNR.ndec{2}
                   UFCMA.log{2} /\
              check_plaintext BNR.lenc{1} p{1} ).
-        + by ecall (equ_cc n{1} ROin.m{1} ROout.m{1}); rewrite /check_plaintext; auto => /> /#.
+        + by ecall (equ_cc n{1} ROin.m{1} ROout.m{1}); auto => /> /#.
         inline{1} 5; inline{1} 8.
         rcondt{1} ^if.
         + by move=> &m; auto => />; rewrite /SplitD.test /= C.insubdK //=; smt(C.gt0_max_counter).