X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpr.ma;h=6db05fe53788180bc2a416e25cc1b2b1979a963d;hb=7e06d9d148ae04a21943377debd933a742d0c2fa;hp=ad4fcb3135663f1c02fd4ed5f5d0a825be5ab376;hpb=3167db4903eea2eddc60a91cfd922be3672ce077;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 ad4fcb313..6db05fe53 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -54,9 +54,9 @@ lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr.
 | #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
   elim (lsubr_fwd_drop2_abbr … HL12 … HLK1) -L1 *
   /3 width=6 by cpr_delta/
-|3,7: /4 width=1 by lsubr_bind, cpr_bind, cpr_beta/
+|3,7: /4 width=1 by lsubr_pair, cpr_bind, cpr_beta/
 |4,6: /3 width=1 by cpr_flat, cpr_eps/
-|5,8: /4 width=3 by lsubr_bind, cpr_zeta, cpr_theta/
+|5,8: /4 width=3 by lsubr_pair, cpr_zeta, cpr_theta/
 ]
 qed-.