X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpx_lift.ma;h=76b7e04119219eabf386c92fc46abae968c4765a;hb=37e1b4f314ffae815beca71300688040f8da6939;hp=d16ff6b2ec420d9e23fec6e3a255a59951cfb34a;hpb=c60524dec7ace912c416a90d6b926bee8553250b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index d16ff6b2e..76b7e0411 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -119,7 +119,7 @@ lemma cpx_inv_lift1: ∀h,g,G. d_deliftable_sn (cpx h g G).
   elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpx_flat, lift_flat, ex2_intro/
 | #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #l #m #HLK #X #H
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+  elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1 by drop_skip/ -L -U1 #T #HTU #HT1
   elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
 | #G #L #V #U1 #U2 #_ #IHU12 #K #s #l #m #HLK #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct