X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_isfin.ma;h=b73e34cea2fcba9b4fcd4d5dcd5022516adf5389;hb=926796df5884453d8f0cf9f294d7776d469ef45b;hp=8a127b35998fd15115db47270d5ca55214fc04cf;hpb=e06774421eb3b8f4438a6876cc1ab4262ef16f6e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
index 8a127b359..b73e34cea 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
@@ -74,5 +74,11 @@ qed.
 (* Inversion lemmas with tail ***********************************************)
 
 lemma isfin_inv_tl: ∀f. 𝐅⦃⫱f⦄ → 𝐅⦃f⦄.
-#f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/   
+#f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/
+qed-.
+
+(* Inversion lemmas with tls ********************************************************)
+
+lemma isfin_inv_tls: ∀n,f. 𝐅⦃⫱*[n]f⦄ → 𝐅⦃f⦄.
+#n elim n -n /3 width=1 by isfin_inv_tl/
 qed-.