- ldrop is now drop as in basic_1

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
index 48fa090bd4145d0b47f78925dc5fba7d11c9462f..001f2017f5fdff5528aa0e9836589c288d0bc662 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
@@ -15,24 +15,16 @@
 include "basic_2/reduction/cpr_lift.ma".
 include "basic_2/reduction/cnr.ma".
 
-(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************)
 
 (* Advanced properties ******************************************************)
 
-(* Basic_1: was only: nf2_csort_lref *)
-lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
-#G #L #i #HL #X #H
-elim (cpr_inv_lref1 … H) -H // *
-#K #V1 #V2 #HLK #_ #_
-lapply (ldrop_mono … HL … HLK) -L #H destruct
-qed.
-
 (* Basic_1: was: nf2_lref_abst *)
 lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
 #G #L #K #V #i #HLK #X #H
 elim (cpr_inv_lref1 … H) -H // *
 #K0 #V1 #V2 #HLK0 #_ #_
-lapply (ldrop_mono … HLK … HLK0) -L #H destruct
+lapply (drop_mono … HLK … HLK0) -L #H destruct
 qed.
 
 (* Relocation properties ****************************************************)