X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Freduction%2Flcpr.ma;h=f01daabceebe6589b793835b561b88b415913897;hb=b4240d93f7fd4c3e60d3495dc558edfc0e0f48e7;hp=03ed43683e6904694a0ed30b3baf5403271fbfa7;hpb=b264ad188cb0023a16dae105b037357fa75c5c1a;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma
index 03ed43683..f01daabce 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma
@@ -16,7 +16,7 @@ include "Basic-2/reduction/cpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
 
-inductive lcpr: lenv → lenv → Prop ≝
+inductive lcpr: relation lenv ≝
 | lcpr_sort: lcpr (⋆) (⋆)
 | lcpr_item: ∀K1,K2,I,V1,V2.
              lcpr K1 K2 → K2 ⊢ V1 ⇒ V2 → lcpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)