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

diff --git a/helm/software/matita/nlibrary/algebra/bool.ma b/helm/software/matita/nlibrary/algebra/bool.ma
index c3a7c6781..0e171fc58 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; //;
+#A; #a; #P; #p; #b; #E; ncases E in p; nauto;
 nqed. 
 
 nlemma csc :