propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / rtmap_isfin.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma
index 5439f36eebd06f2010c31c052482b6546ac9ba87..7da7f85ad0d313eb650dc5563878033ba14abe8d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma
@@ -67,13 +67,13 @@ qed.
 (* Properties with iterated push ********************************************)
 
 lemma isfin_pushs: ∀n,f. 𝐅❪f❫ → 𝐅❪⫯*[n]f❫.
-#n elim n -n /3 width=3 by isfin_push/
+#n @(nat_ind_succ … n) -n /3 width=3 by isfin_push/
 qed.
 
 (* Inversion lemmas with iterated push **************************************)
 
 lemma isfin_inv_pushs: ∀n,g. 𝐅❪⫯*[n]g❫ → 𝐅❪g❫.
-#n elim n -n /3 width=3 by isfin_inv_push/
+#n @(nat_ind_succ … n) -n /3 width=3 by isfin_inv_push/
 qed.
 
 (* Properties with tail *****************************************************)
@@ -92,5 +92,5 @@ qed-.
 (* Inversion lemmas with iterated tail **************************************)
 
 lemma isfin_inv_tls: ∀n,f. 𝐅❪⫱*[n]f❫ → 𝐅❪f❫.
-#n elim n -n /3 width=1 by isfin_inv_tl/
+#n @(nat_ind_succ … n) -n /3 width=1 by isfin_inv_tl/
 qed-.