X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpr.ma;h=421cc97de94ddb8cec4567a715de574843b0f888;hb=0679e5d5a305a43a8b4b01a5ac4c7caffacc73b9;hp=e6ad7b2bac33235f086ad727f68cad5ec9152609;hpb=73428212ec1db9ea1559994f88cd02894a2c9478;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index e6ad7b2ba..421cc97de 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -45,16 +45,11 @@ interpretation "context-sensitive parallel reduction (term)"
 
 (* Basic properties *********************************************************)
 
-(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
-                       ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
+lemma cpr_lsubr_trans: lsubr_trans … cpr.
 #L1 #T1 #T2 #H elim H -L1 -T1 -T2
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
-  lapply (ldrop_fwd_O1_length … HLK1) #H2i
-  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
-  <H2i -H2i <minus_plus_m_m /3 width=6/
+  elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -HL12 -HLK1 /3 width=6/
 |3,7: /4 width=1/
 |4,6: /3 width=1/
 |5,8: /4 width=3/