X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpm_lsubr.ma;h=4b246a2832792eaeb14e03a1e47f285de6ba0ce4;hb=747b42f3b9aac5487047f57742f1fcf05b56b57d;hp=ac03ed30cabea02715faf9b02f6ee5516a9dba8d;hpb=5a81feec7b8c07a43e96d772431e06bad177ed8c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma
index ac03ed30c..4b246a283 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma
@@ -23,11 +23,3 @@ include "basic_2/rt_transition/cpm.ma".
 lemma lsubr_cpm_trans: ∀n,h,G. lsub_trans … (cpm n h G) lsubr.
 #n #h #G #L1 #T1 #T2 * /3 width=5 by lsubr_cpg_trans, ex2_intro/
 qed-.
-
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was by definition: pr2_free *)
-(* Basic_2A1: includes: tpr_cpr *)
-lemma tpm_cpm: ∀n,h,G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡[n, h] T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2.
-#n #h #G #T1 #T2 #HT12 #L lapply (lsubr_cpm_trans … HT12 L ?) //
-qed.