X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_drops.ma;h=441d3c51f5670ff8298c9f8f35738024078f3102;hb=0c7cb3c503c0fcab104ad89ebc88683dc9830d06;hp=47b1eec39bf521620484da8350e588a25f8303a7;hpb=5b93ea047903b606979705ed25a6df6504fd027c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
index 47b1eec39..441d3c51f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
@@ -12,8 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/relocation/nstream_coafter.ma".
 include "basic_2/relocation/drops_drops.ma".
-include "basic_2/static/frees.ma".
+include "basic_2/static/frees_frees.ma".
 
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
 
@@ -142,6 +143,13 @@ lemma frees_lifts: ∀b,f1,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f1 →
 ]
 qed-.
 
+(* Forward lemmas with generic slicing for local environments ***************)
+
+lemma frees_fwd_coafter: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →
+                         ∀f,K. ⬇*[b, f] L ≡ K → ∀T. ⬆*[f] T ≡ U →
+                         ∀f1. K ⊢ 𝐅*⦃T⦄ ≡ f1 → f ~⊚ f1 ≡ f2.
+/4 width=11 by frees_lifts, frees_mono, coafter_eq_repl_back0/ qed-.
+
 (* Inversion lemmas with generic slicing for local environments *************)
 
 lemma frees_inv_lifts: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →