update in ground_2 and basic_2 ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
index 6aac2af44da004b28e098d83c20b2616304177b4..00973b22082efd264038d0c8de8b52210bef8400 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
@@ -85,7 +85,7 @@ theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T →
     lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i
     elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1
     @ex2_intro [2: /2 width=1/ | skip ] -Hd1e12
-    @lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ]
+    @lift_lref_ge_minus_eq [ >plus_minus_associative // | /2 width=1/ ]
   ]
 | #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/
 | #a #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2