remove unnecessary rewrite /...

EasyCrypt · Dec 6, 2023 · a76cc78 · a76cc78
1 parent 4ff34a2
commit a76cc78
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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).