X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_preserve_cpes.ma;h=60fc0d0daacff9da2c426afd9574dc8c580c9ed8;hp=f266bb5813fe1ba8aa6dbf88a8ecb2d62d45dc23;hb=a0b7db9844126ebcdf4b5dbb586514854cef5d93;hpb=31be09cc0d040577917783e050e1d38c0daa8f01

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma
index f266bb581..60fc0d0da 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma
@@ -39,14 +39,3 @@ elim (eq_term_dec U1 U2) [ #H destruct | #HnU12 ]
   /3 width=6 by cpre_mono/
 ]
 qed-.
-
-(* Advanced inversion lemmas with t-bound rt-equivalence for terms **********)
-
-lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
-      ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
-      ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
-                 ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
-#a #h #G #L #V #T #H
-elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
-/3 width=7 by cpms_div, ex5_4_intro/
-qed-.