X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Freducibility%2Ftpr_lift.ma;h=32a80aafc83c7e74ef166e42d7a0d6a846481510;hb=0aa60d67f17b528b896e05bbd01038cbc195f69d;hp=d9d9c549a918c60b919f3d341a689576d9ae23bd;hpb=62a926c1a14562bf158941156c6032c0c8d86fbe;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
index d9d9c549a..32a80aafc 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
@@ -21,7 +21,7 @@ include "Basic_2/reducibility/tpr.ma".
 
 (* Basic_1: was: pr0_lift *)
 lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
-                ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2.
+                ∀d,e,U1. ⇑[d, e] T1 ≡ U1 → ∀U2. ⇑[d, e] T2 ≡ U2 → U1 ⇒ U2.
 #T1 #T2 #H elim H -T1 -T2
 [ * #i #d #e #U1 #HU1 #U2 #HU2
   lapply (lift_mono … HU1 … HU2) -HU1 #H destruct
@@ -58,8 +58,8 @@ qed.
 
 (* Basic_1: was: pr0_gen_lift *)
 lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
-                    ∀d,e,U1. ↑[d, e] U1 ≡ T1 →
-                    ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2.
+                    ∀d,e,U1. ⇑[d, e] U1 ≡ T1 →
+                    ∃∃U2. ⇑[d, e] U2 ≡ T2 & U1 ⇒ U2.
 #T1 #T2 #H elim H -T1 -T2
 [ * #i #d #e #U1 #HU1
   [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/