Release 0.5.9.

[helm.git] / helm / software / matita / nlibrary / algebra / bool.ma

diff --git a/helm/software/matita/nlibrary/algebra/bool.ma b/helm/software/matita/nlibrary/algebra/bool.ma
index c3a7c6781a1317b479dd0cb2a387d063c67aca2a..0e171fc584911d4f41b35d2a6b22cfb3d7a945d6 100644 (file)
--- 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 :