X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Flpr_lpr.ma;h=fad8b481a731d9b4873c58dc7ef36e2ce6cbf8cd;hb=37e1b4f314ffae815beca71300688040f8da6939;hp=284fafe2035b697917901c6a2e24cf80c77aed09;hpb=c60524dec7ace912c416a90d6b926bee8553250b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index 284fafe20..fad8b481a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -244,7 +244,7 @@ fact cpr_conf_lpr_beta_beta:
 #a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01
 #V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
-elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2
+elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ #W #HW1 #HW2
 elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
 lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/
 lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/