- the confluence of context-senstitive parallel reduction (cpr) is closed!

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

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
index 75652795873f3f29b204ca4f0a7e7a7c83d6c89f..fce71d15a9caa2e2e59da4e2f037a2dff454468f 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
@@ -91,7 +91,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
                                  ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
                                  U2 = 𝕓{I} V2. T
                      ) ∨
-                     ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
+                     ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
 /2/ qed.
 
 (* Basic-1: was pr0_gen_abbr *)
@@ -100,7 +100,7 @@ lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
                                  ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
                                  U2 = 𝕓{Abbr} V2. T
                       ) ∨
-                      ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
+                      ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
 #V1 #T1 #U2 #H
 elim (tpr_inv_bind1 … H) -H * /3 width=7/
 qed.