- support for transitive closures started

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / reduction / lcpr.ma

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 03ed43683e6904694a0ed30b3baf5403271fbfa7..f01daabceebe6589b793835b561b88b415913897 100644 (file)
--- 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) (*𝕓*)