X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Freduction%2Ftpr_defs.ma;h=bddd93017bf8851b2e731b81c3d0c9ce964db7b5;hb=dd88a8fa58d50833118cadd96ba8e3bcf70340a4;hp=29f8ae4e7797ae70e8d85a4ced455d331ba71cbc;hpb=6f29b61aeae23efb412ac48ab747d63bcedcacd6;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
index 29f8ae4e7..bddd93017 100644
--- a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/substitution/subst_defs.ma".
+include "lambda-delta/substitution/ps_defs.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
@@ -23,9 +23,8 @@ inductive tpr: term → term → Prop ≝
 | tpr_beta : ∀V1,V2,W,T1,T2.
              tpr V1 V2 → tpr T1 T2 →
              tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
-| tpr_delta: ∀V1,V2,T1,T2,T0,T.
-             tpr V1 V2 → tpr T1 T2 →
-             ⋆.  𝕓{Abbr} V2 ⊢ ↓[0, 1] T2 ≡ T0 → ↑[0, 1] T0 ≡ T →
+| tpr_delta: ∀V1,V2,T1,T2,T.
+             tpr V1 V2 → tpr T1 T2 → ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T →
              tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} V2. T)
 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
              tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
@@ -37,7 +36,7 @@ inductive tpr: term → term → Prop ≝
 
 interpretation
    "context-free parallel reduction (term)"
-   'PR T1 T2 = (tpr T1 T2).
+   'PRed T1 T2 = (tpr T1 T2).
 
 (* Basic properties *********************************************************)
 
@@ -59,7 +58,7 @@ lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
 | #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V1 #V2 #T1 #T2 #T0 #T #_ #_ #_ #_ #_ #_ #i #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #_ #_ #i #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct
 | #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/
 | #V #T1 #T2 #HT12 #_ #i #H destruct /3/