update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_sle.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
index c357babf95089d5ebc22eb8918770c6b843ff0d2..fb59fcb786e84c360886d3642fdf2843e9ae6660 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
@@ -146,6 +146,12 @@ lemma sle_inv_tl_dx: ∀f1,f2. f1 ⊆ ⫱f2 → ↑f1 ⊆ f2.
 /2 width=5 by sle_push, sle_weak/
 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/
+qed.
+
 (* Properties with isid *****************************************************)
 
 corec lemma sle_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊆ f2.