- inversion lemmas for tpr completed!

[helm.git] / matita / matita / lib / lambda-delta / reduction / lpr_defs.ma

diff --git a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
index dab96f2dd871a19a0c8d47a543d8dc8f6ef2f2e9..2411191084e4856e99c3704b8ecf3bcc2f6b5fa6 100644 (file)
--- a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
+++ b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
@@ -24,7 +24,7 @@ inductive lpr: lenv → lenv → Prop ≝
 
 interpretation
   "context-free parallel reduction (environment)"
-  'PR L1 L2 = (lpr L1 L2).
+  'PRed L1 L2 = (lpr L1 L2).
 
 (* Basic inversion lemmas ***************************************************)