Dummy dependent types are no longer cleaned in inductive type arities.

[helm.git] / helm / software / matita / library / nat / neper.ma

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 8da13d9ab08e7fdbb4d7f165e75394eb69af15b4..f5847033ab0305660fff7faa26f2a2852811e41f 100644 (file)
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -280,7 +280,7 @@ rewrite > lt_O_to_div_times
      assumption
     |apply lt_exp_Sn_n_SSSO
     ]
-  |apply (O_lt_times_to_O_lt ? n2).
+  |apply (O_lt_times_to_O_lt ? n1).
    rewrite < H2.
    assumption
   ]