X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops.ma;h=1fc24f51e56e63b193c619a26c8c9436c8164131;hb=d3636c8688ec08cc39eb7ce6c1918b25bbccc349;hp=09d381cd82ccfaee34b9f7428e06d22b6fb8036c;hpb=7fff13721f6e7040e76faad31583b1cb86693d2c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index 09d381cd8..1fc24f51e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -12,11 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/relocation/rtmap_isfin.ma".
 include "basic_2/notation/relations/rdropstar_4.ma".
 include "basic_2/relocation/lreq.ma".
 include "basic_2/relocation/lifts.ma".
 
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
 
 (* Basic_1: includes: drop_skip_bind drop1_skip_bind *)
 (* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip
@@ -203,6 +204,13 @@ qed-.
 lemma drops_isuni_fwd_drop2: ∀I,X,K,V,c,f. 𝐔⦃f⦄ → ⬇*[c, f] X ≡ K.ⓑ{I}V → ⬇*[c, ⫯f] X ≡ K.
 /3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-.
 
+(* forward lemmas with test for finite colength *****************************)
+
+lemma drops_fwd_isfin: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐅⦃f⦄.
+#L1 #L2 #f #H elim H -L1 -L2 -f
+/3 width=1 by isfin_next, isfin_push, isfin_isid/
+qed-.
+
 (* Basic_2A1: removed theorems 14:
               drops_inv_nil drops_inv_cons d1_liftable_liftables
               drop_refl_atom_O2