X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Fcnx%2Fcnx_lift.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Fcnx%2Fcnx_lift.etc;h=0000000000000000000000000000000000000000;hb=b4b5f03ffca4f250a1dc02f277b70e4f33ac8a9b;hp=121b0d5e262cc78c2c1a4074bcdd5fae0dd6ad4c;hpb=09b4420070d6a71990e16211e499b51dbb0742cb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_lift.etc
deleted file mode 100644
index 121b0d5e2..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cnx/cnx_lift.etc
+++ /dev/null
@@ -1,37 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/cnx.ma".
-
-(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************)
-
-(* Relocation properties ****************************************************)
-
-lemma cnx_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⬇[c, l, k] L0 ≡ L →
-                ⬆[l, k] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄.
-#h #o #G #L0 #L #T #T0 #c #l #k #HLT #HL0 #HT0 #X #H
-elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
-<(HLT … HT1) in HT0; -L #HT0
->(lift_mono … HT10 … HT0) -T1 -X //
-qed.
-
-lemma cnx_inv_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄ → ⬇[c, l, k] L0 ≡ L →
-                    ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
-#h #o #G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H
-elim (lift_total X l k) #X0 #HX0
-lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0
->(HLT0 … HTX0) in HX0; -L0 -X0 #H
->(lift_inj … H … HT0) -T0 -X -l -k //
-qed-.