frees_drops, initial versrion

[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 0c9a65bf272f37af91ccd057b8bc2bce390659ce..8a127b35998fd15115db47270d5ca55214fc04cf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
@@ -70,3 +70,9 @@ lemma isfin_tl: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫱f⦄.
 #f elim (pn_split f) * #g #H #Hf destruct
 /3 width=3 by isfin_fwd_push, isfin_inv_next/
 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/   
+qed-.