X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Falgebra%2Fbool.ma;h=c3a7c6781a1317b479dd0cb2a387d063c67aca2a;hb=34311f3f810eb893b865d1893eae1cf62cd490b4;hp=0e171fc584911d4f41b35d2a6b22cfb3d7a945d6;hpb=b7555a8732a9a304ac45c4e8024f122e261506af;p=helm.git

diff --git a/helm/software/matita/nlibrary/algebra/bool.ma b/helm/software/matita/nlibrary/algebra/bool.ma
index 0e171fc58..c3a7c6781 100644
--- a/helm/software/matita/nlibrary/algebra/bool.ma
+++ b/helm/software/matita/nlibrary/algebra/bool.ma
@@ -24,7 +24,7 @@ nlemma eq_ind_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.a
 nqed.
 
 nlemma eq_ind_r_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.b = a → P b.
-#A; #a; #P; #p; #b; #E; ncases E in p; nauto;
+#A; #a; #P; #p; #b; #E; ncases E in p; //;
 nqed. 
 
 nlemma csc :