X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms_cpms.ma;h=fcd97f3b905b5192dc3c7cc908bfebe0ef7bab2a;hp=23d0295ca94e8464aaeb3eb4c2ff029def87f670;hb=084ea7868f6153effc18e8ee1c0e6cdb34d181c0;hpb=de3a41b9a4e51dc1b09adce800273adf5ffa1215

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
index 23d0295ca..fcd97f3b9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
@@ -176,19 +176,3 @@ theorem cpms_trans_swap (h) (G) (L) (T1):
 lapply (cpms_trans … HT1 … HT2) -T <commutative_plus #HT12
 /2 width=1 by cpms_inv_plus/
 qed-.
-
-(* More advanced inversion lemmas *******************************************)
-(*
-lemma cpms_inv_appl_sn_decompose (h) (n) (G) (L) (V1) (T1):
-      ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ➡*[n,h] X2 →
-      ∃∃T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⓐV1.T2 ➡*[h] X2.
-#h #n #G #L #V1 #T1 #X2 #H
-@(cpms_ind_dx … H) -n -X2
-[ /2 width=3 by ex2_intro/
-| #n1 #n2 #X #X2 #_ * #X1 #HTX1 #HX1 #HX2
-  elim (pippo … HX1 … HX2) -X #X #HX1 #HX2
-  elim (cpm_inv_appl_sn_decompose … HX1) -HX1 #U1 #HXU1 #HU1X
-  /3 width=5 by cprs_step_sn, cpms_step_dx, ex2_intro/
-]
-qed-.
-*)