X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees.ma;h=5911dddfec361647781617494411dd91c5092e6f;hb=52616a7a6a550efd75ed56e7e246132453506002;hp=3699063ce1ef280c3e1afddcc64a28015bac12e7;hpb=6a4711dbb4bec52222e9d0586326ef03b9fbc81b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
index 3699063ce..5911dddfe 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
@@ -146,6 +146,24 @@ 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/  
+]
+qed-.
+
+lemma frees_inv_lref_pair: ∀f,I,K,V,i. K.ⓑ{I}V ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
+                           ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
+#f #I #K #V #i #H elim (frees_inv_lref … H) -H *
+[ #H destruct
+| #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/  
+]
+qed-.
+
 (* Basic forward lemmas ****************************************************)
 
 lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄.