- some renaming

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

diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
index 29f8ae4e7797ae70e8d85a4ced455d331ba71cbc..bddd93017bf8851b2e731b81c3d0c9ce964db7b5 100644 (file)
--- 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/