normal forms for extended substitution

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cnx_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
index 65c035f4ac2feb6d58366dfa02b6f46fd3aaae66..7f3bedbd012d0436764c6d549d8de9b324d95d9f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
@@ -17,15 +17,6 @@ include "basic_2/reduction/cnx.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************)
 
-(* Advanced properties ******************************************************)
-
-lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄.
-#h #g #G #L #i #HL #X #H
-elim (cpx_inv_lref1 … H) -H // *
-#I #K #V1 #V2 #HLK #_ #_
-lapply (ldrop_mono … HL … HLK) -L #H destruct
-qed.
-
 (* Relocation properties ****************************************************)
 
 lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⇩[s, d, e] L0 ≡ L →