apply and auto.equational_case call saturation.solve_narrowing

[helm.git] / helm / software / matita / library / Q / nat_fact / times.ma

diff --git a/helm/software/matita/library/Q/nat_fact/times.ma b/helm/software/matita/library/Q/nat_fact/times.ma
index 43c213c9b3f00b6de8e38f13f98efb7a324598bf..88e2602b886f79f5023750ae9de76578934ba164 100644 (file)
--- a/helm/software/matita/library/Q/nat_fact/times.ma
+++ b/helm/software/matita/library/Q/nat_fact/times.ma
@@ -30,7 +30,7 @@ let rec times_f h g \def
 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
 =defactorize_aux g m*defactorize_aux h m.
 intro.elim g
-  [elim h;simplify;autobatch
+  [elim h;simplify;autobatch;
   |elim h
     [simplify;autobatch
     |simplify.rewrite > (H n3 (S m)).autobatch