X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fminimization.ma;h=4c55ea6beb9b37a91e752913a0338786cea24952;hb=7da6488b45e5dfc1b675552a7f19c58a6abbff2b;hp=eda9d016618d1031be5b126b65b35ca105b9ee11;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index eda9d0166..4c55ea6be 100644
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -122,7 +122,7 @@ qed.
 theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) → 
   max n f = max n g.
 #f #g #n (elim n) //
-#m #Hind #ext normalize >ext >Hind //
+#m #Hind #ext normalize >ext normalize in Hind >Hind //
 #i #ltim @ext /2/
 qed.