X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_istot.ma;h=d4e80390ff447878ad9ae93bc2cb7e001644874c;hb=ad3d1cac216cf3882e4adf691b27c00838c6b9b1;hp=07b24f9732c38bec2a9bd8e97b2708f539eeaa56;hpb=b9526dac808d40bf89dc378cf9c5ea0c121526a4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
index 07b24f973..d4e80390f 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
@@ -36,14 +36,14 @@ qed-.
 
 (* Properties on tl *********************************************************)
 
-lemma istot_tl: ∀f. 𝐓⦃f⦄ → 𝐓⦃↓f⦄.
+lemma istot_tl: ∀f. 𝐓⦃f⦄ → 𝐓⦃⫱f⦄.
 #f cases (pn_split f) *
 #g * -f /2 width=3 by istot_inv_next, istot_inv_push/
 qed.
 
-(* Properties on minus ******************************************************)
+(* Properties on tls ********************************************************)
 
-lemma istot_minus: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃f-n⦄.
+lemma istot_tls: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃⫱*[n]f⦄.
 #n elim n -n /3 width=1 by istot_tl/
 qed.