X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Frtmap_isdiv.ma;h=fa421497a194bf9d174e342f71325bb55b59bab1;hp=1b6ce598e938e4991512b6b30ffdbca2f05527cb;hb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;hpb=77c9255de3c5f7780aeacd745703a1cc76328a68

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma
index 1b6ce598e..fa421497a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma
@@ -79,13 +79,13 @@ qed-.
 (* Properties with iterated next ********************************************)
 
 lemma isdiv_nexts: ∀n,f. 𝛀❪f❫ → 𝛀❪↑*[n]f❫.
-#n elim n -n /3 width=3 by isdiv_next/
+#n @(nat_ind_succ … n) -n /3 width=3 by isdiv_next/
 qed.
 
 (* Inversion lemmas with iterated next **************************************)
 
 lemma isdiv_inv_nexts: ∀n,g. 𝛀❪↑*[n]g❫ → 𝛀❪g❫.
-#n elim n -n /3 width=3 by isdiv_inv_next/
+#n @(nat_ind_succ … n) -n /3 width=3 by isdiv_inv_next/
 qed.
 
 (* Properties with tail *****************************************************)
@@ -100,5 +100,5 @@ qed.
 (* Properties with iterated tail ********************************************)
 
 lemma isdiv_tls: ∀n,g. 𝛀❪g❫ → 𝛀❪⫱*[n]g❫.
-#n elim n -n /3 width=1 by isdiv_tl/
+#n @(nat_ind_succ … n) -n /3 width=1 by isdiv_tl/
 qed.