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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma
index edd962354..002e6eac7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma
@@ -111,10 +111,11 @@ corec theorem sle_trans: Transitive … sle.
 /3 width=5 by sle_push, sle_next, sle_weak/
 qed-.
 
-(* Properties with iteraded push ********************************************)
+(* Properties with iterated push ********************************************)
 
-lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀i. ⫯*[i] f1 ⊆ ⫯*[i] f2.
-#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_push/
+lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀n. ⫯*[n] f1 ⊆ ⫯*[n] f2.
+#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n
+/2 width=5 by sle_push/
 qed.
 
 (* Properties with tail *****************************************************)
@@ -148,8 +149,9 @@ qed-.
 
 (* Properties with iteraded tail ********************************************)
 
-lemma sle_tls: ∀f1,f2. f1 ⊆ f2 → ∀i. ⫱*[i] f1 ⊆ ⫱*[i] f2.
-#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_tl/
+lemma sle_tls: ∀f1,f2. f1 ⊆ f2 → ∀n. ⫱*[n] f1 ⊆ ⫱*[n] f2.
+#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n
+/2 width=5 by sle_tl/
 qed.
 
 (* Properties with isid *****************************************************)