X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Freduction%2Ftpr_lift.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Freduction%2Ftpr_lift.ma;h=f06d8980aa3d2ccf50477dcad74caf50330ef67a;hb=0466f6387b02f1d0644fb74eacca237e30589111;hp=412a0a2ede2041bd801611e1c78bbcdf5d9d4102;hpb=dc21a7ae8ac838b0967db8d65ca30724ae556a47;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
index 412a0a2ed..f06d8980a 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
@@ -17,6 +17,7 @@ include "Basic-2/reduction/tpr.ma".
 
 (* Relocation properties ****************************************************)
 
+(* 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.
 #T1 #T2 #H elim H -H T1 T2
@@ -52,6 +53,7 @@ lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
 ]
 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.
@@ -109,6 +111,7 @@ fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1
 ]
 qed.
 
+(* Basic-1: was pr0_gen_abst *)
 lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
                      ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
 /2/ qed.