other addition to the standard library removed

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / lift_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
index 3f5b8ab6a9e3a48af758f799267d18592c9e3f15..cfcf976e00bbfd07dc73e8d9d2e1ac59c3e56699 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma
@@ -126,7 +126,7 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
   elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct /3 width=3/ /4 width=3/
 | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21
   lapply (transitive_le … Hd21 Hid1) -Hd21 #Hid2
-  lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=1/ #HX destruct
+  lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3/ #HX destruct
   >plus_plus_comm_23 /4 width=3/
 | #p #d1 #e1 #d2 #e2 #X #HX #_
   >(lift_inv_gref1 … HX) -HX /2 width=3/