lfpx_drops completed!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / frees_drops.ma

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 47b1eec39bf521620484da8350e588a25f8303a7..441d3c51f5670ff8298c9f8f35738024078f3102 100644 (file)
--- 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 →