X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fcologic.ma;h=8b9ed3c15d450c622d78eb42294f43a98d145922;hb=bf7be462a06e739b39af20f72362857e849a2aa0;hp=ca4921607b6b5d4d5ec1e232f63b3be1ca4a54de;hpb=e17c4da82bd52712f03c112660c52eb8f1783843;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/cologic.ma b/helm/software/matita/nlibrary/logic/cologic.ma
index ca4921607..8b9ed3c15 100644
--- a/helm/software/matita/nlibrary/logic/cologic.ma
+++ b/helm/software/matita/nlibrary/logic/cologic.ma
@@ -95,7 +95,7 @@ ntheorem cand_true: ∀c1,c2. ceq c1 (certain true) → ceq (cand c1 c2) c2.
            ##[ nlapply (KK2 EE); #XX; nrewrite > (cand_truer …) in XX; #YY;
                @3;
                
-           ##[ nrewrite > (ccases (cand (maybe xx) (certain true)));
+           rewrite > (ccases (cand (maybe xx) (certain true)));
                nnormalize; @3; @2;