update in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crf_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crf_append.ma
index 7d3ac6050f66f1f41ec3a2449529921c3d3b770c..0a86278d06d29c162331ed1ff8995c6a40ebbffc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crf_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crf_append.ma
@@ -22,7 +22,7 @@ include "basic_2/reduction/crf.ma".
 lemma crf_labst_last: ∀L,T,W. L ⊢ 𝐑⦃T⦄  → ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄.
 #L #T #W #H elim H -L -T /2 width=1/
 #L #K #V #i #HLK
-lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
+lapply (ldrop_fwd_length_lt2 … HLK) #Hi
 lapply (ldrop_O1_append_sn_le … HLK … (⋆.ⓛW)) -HLK /2 width=2/ -Hi /2 width=3/
 qed.
 
@@ -36,14 +36,14 @@ fact crf_inv_labst_last_aux: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄  →
                              ∀L2. L1 = ⋆.ⓛW @@ L2 → L2 ⊢ 𝐑⦃T⦄.
 #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
 [ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
-  lapply (ldrop_fwd_ldrop2_length … HLK1)
+  lapply (ldrop_fwd_length_lt2 … HLK1)
   >append_length >commutative_plus normalize in ⊢ (??% → ?); #H
   elim (le_to_or_lt_eq i (|L2|) ?) /2 width=1/ -H #Hi destruct
   [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2
     lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi
     normalize #H destruct /2 width=3/
   | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // <minus_n_n #H
-    lapply (ldrop_inv_refl … H) -H #H destruct
+    lapply (ldrop_inv_O2 … H) -H #H destruct
   ]
 | #a #I #L1 #V #T #HI #_ #IHT #L2 #H destruct /3 width=1/
 ]