X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fdelift_lift.ma;h=a53033aa0c7e73752848c6437b37436571bc6160;hb=cc21d0caa6229b7d1a905f9b62de2af4f40cc863;hp=9fe72f82dd696ed4bb55dee57a1d351dcaa14194;hpb=5ea90cbbb01fe0bf3b77221d9e6c87002982621f;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
index 9fe72f82d..a53033aa0 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
@@ -37,7 +37,7 @@ fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 
   elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
   elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
   lapply (lt_to_le_to_lt … Hide Hde) #Hi
-  elim (ldrop_O1 … Hi) -Hi #I #K #V1 #HLK
+  elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK
   lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
   lapply (ldrop_pair2_fwd_cw … HLK (#i)) #HKL
   lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
@@ -47,7 +47,7 @@ fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 
   elim (IH … HKL … HK ?) -IH -HKL -HK
   [3: // |2: skip |4: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *)
   elim (lift_total V2 0 d) /3 width=7/
-| #I #V1 #T1 #d #e #Hde #HL #H destruct
+| #a #I #V1 #T1 #d #e #Hde #HL #H destruct
   elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12
   elim (IH (L.ⓑ{I}V1) T1 ? ? (d+1) e ? ? ?) -IH [3,6: // |2: skip |4,5: /2 width=1/ ] -Hde -HL #T2 #HT12
   lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/