- improved Makefile esp. with the "trim" function

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lift_lift.ma

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 3e18bff3275543a3d1daf190235cd529f928ec72..804c903d182a9d164e27fb7fc498ebd6f87d8d33 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma
@@ -84,7 +84,7 @@ theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T →
   | >(lift_inv_lref2_ge … H ?) -H //
     lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i
     elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1
-    @ex2_1_intro [2: /2 width=1/ | skip ] -Hd1e12
+    @ex2_intro [2: /2 width=1/ | skip ] -Hd1e12
     @lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ]
   ]
 | #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/
@@ -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 //