X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs_lift.ma;h=9ff2b6f2c196fd21b651243fb9070f15990f5241;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=1d5a3e778afeedb73f2b54c4ec2823e518c5c5c1;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma
index 1d5a3e778..9ff2b6f2c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma
@@ -40,7 +40,7 @@ lemma lstas_cpxs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 →
 | #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #d1 #H #Hd21
   elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0
   lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
-  #HV1 #H destruct lapply (le_plus_to_le_r … Hd21) -Hd21
+  #HV1 #H destruct lapply (le_plus_to_le_c … Hd21) -Hd21
   /3 width=7 by cpxs_delta/
 | /4 width=3 by cpxs_bind_dx, da_inv_bind/
 | /4 width=3 by cpxs_flat_dx, da_inv_flat/