first definition of cpm:

[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 681e07d8c701474386cf75c5abb2cea7da2a7155..c5762eacbbe202d8c246ec8f26d0bb63782efc5f 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,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/relocation/rtmap_coafter.ma".
+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 *****************************************)
 
@@ -49,7 +49,8 @@ lemma frees_lref_pushs: ∀f,K,j. K ⊢ 𝐅*⦃#j⦄ ≡ f →
                         ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃#(i+j)⦄ ≡ ↑*[i] f.
 #f #K #j #Hf #i elim i -i
 [ #L #H lapply (drops_fwd_isid … H ?) -H //
-| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_lref/
+| #i #IH #L #H elim (drops_inv_succ … H) -H
+  #I #Y #V #HYK #H destruct /3 width=1 by frees_lref/
 ]
 qed.
 
@@ -143,6 +144,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 →