work in progress on frees_drops

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

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 8a127b35998fd15115db47270d5ca55214fc04cf..b73e34cea2fcba9b4fcd4d5dcd5022516adf5389 100644 (file)
--- 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-.