X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Flpr.ma;h=01966eefb03b9f415c84720c625d9ccac61f9284;hb=dffdece065d12d9961a6c3f1222f6d112030336f;hp=fd05f6373d0e0716147d4e3455bbd1630480025b;hpb=87fbbf33fcc2ed91cc8b8a08e1c378ef49ac723d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
index fd05f6373..01966eefb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
@@ -18,7 +18,7 @@ include "basic_2/reduction/cpr.ma".
 
 (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
 
-definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (λ_.cpr G).
+definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (cpr G).
 
 interpretation "parallel reduction (local environment, sn variant)"
    'PRedSn G L1 L2 = (lpr G L1 L2).