update in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
index 25fca957302153500d1adf59128d28d985a0c082..206ec63e4b8a99a4c9d27e9417b680003970730c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
@@ -172,33 +172,6 @@ lemma frees_inv_flat: ∀f,I,L,V,T. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f →
                       ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
 /2 width=4 by frees_inv_flat_aux/ qed-.
 
-(* Advanced inversion lemmas ***********************************************)
-(*
-lemma frees_inv_zero_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≡ f →
-                           ∃∃g. K ⊢ 𝐅*⦃V⦄ ≡ g & f = ⫯g.
-#f #I #K #V #H elim (frees_inv_zero … H) -H *
-[ #H destruct
-| #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
-| #g #Z #Y #_ #H destruct
-]
-qed-.
-
-lemma frees_inv_zero_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≡ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯g.
-#f #I #K #H elim (frees_inv_zero … H) -H *
-[ #H destruct
-| #g #Z #Y #X #_ #H destruct
-| /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma frees_inv_lref_bind: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
-                           ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
-#f #I #K #i #H elim (frees_inv_lref … H) -H *
-[ #H destruct
-| #g #Z #Y #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/  
-]
-qed-.
-*)
 (* Basic properties ********************************************************)
 
 lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
@@ -226,6 +199,12 @@ lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f)
 #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
 qed-.
 
+lemma frees_lref_push: ∀f,i. ⋆ ⊢ 𝐅*⦃#i⦄ ≡ f → ⋆ ⊢ 𝐅*⦃#⫯i⦄ ≡ ↑f.
+#f #i #H
+elim (frees_inv_atom … H) -H #g #Hg #H destruct
+/2 width=1 by frees_atom/
+qed.
+
 (* Forward lemmas with test for finite colength *****************************)
 
 lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄.