X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flift_lift.ma;h=804c903d182a9d164e27fb7fc498ebd6f87d8d33;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=81f2b49a91a044c03a9ed351db4e626493c8bec0;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
index 81f2b49a9..804c903d1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
@@ -103,9 +103,9 @@ theorem lift_mono: ∀d,e,T,U1. ⇧[d,e] T ≡ U1 → ∀U2. ⇧[d,e] T ≡ U2 
 #d #e #T #U1 #H elim H -d -e -T -U1
 [ #k #d #e #X #HX
   lapply (lift_inv_sort1 … HX) -HX //
-| #i #d #e #Hid #X #HX 
+| #i #d #e #Hid #X #HX
   lapply (lift_inv_lref1_lt … HX ?) -HX //
-| #i #d #e #Hdi #X #HX 
+| #i #d #e #Hdi #X #HX
   lapply (lift_inv_lref1_ge … HX ?) -HX //
 | #p #d #e #X #HX
   lapply (lift_inv_gref1 … HX) -HX //