- main lemmas about abstract reducibility candidates closed

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / reducibility / tpr_lift.ma

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 d9d9c549a918c60b919f3d341a689576d9ae23bd..be40639a863d6f7fbe85cbe582ade28fd9f95bcc 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
@@ -20,8 +20,8 @@ include "Basic_2/reducibility/tpr.ma".
 (* Relocation properties ****************************************************)
 
 (* Basic_1: was: pr0_lift *)
-lemma tpr_lift: â\88\80T1,T2. T1 â\87\92 T2 →
-                â\88\80d,e,U1. â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92 U1 â\87\92 U2.
+lemma tpr_lift: â\88\80T1,T2. T1 â\9e¡ T2 →
+                â\88\80d,e,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87§[d, e] T2 â\89¡ U2 â\86\92 U1 â\9e¡ U2.
 #T1 #T2 #H elim H -T1 -T2
 [ * #i #d #e #U1 #HU1 #U2 #HU2
   lapply (lift_mono … HU1 … HU2) -HU1 #H destruct
@@ -57,9 +57,9 @@ lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
 qed.
 
 (* Basic_1: was: pr0_gen_lift *)
-lemma tpr_inv_lift: â\88\80T1,T2. T1 â\87\92 T2 →
-                    â\88\80d,e,U1. â\86\91[d, e] U1 ≡ T1 →
-                    â\88\83â\88\83U2. â\86\91[d, e] U2 â\89¡ T2 & U1 â\87\92 U2.
+lemma tpr_inv_lift: â\88\80T1,T2. T1 â\9e¡ T2 →
+                    â\88\80d,e,U1. â\87§[d, e] U1 ≡ T1 →
+                    â\88\83â\88\83U2. â\87§[d, e] U2 â\89¡ T2 & U1 â\9e¡ U2.
 #T1 #T2 #H elim H -T1 -T2
 [ * #i #d #e #U1 #HU1
   [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/
@@ -101,8 +101,8 @@ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-fact tpr_inv_abst1_aux: â\88\80U1,U2. U1 â\87\92 U2 â\86\92 â\88\80V1,T1. U1 = ð\9d\95\94{Abst} V1. T1 →
-                        â\88\83â\88\83V2,T2. V1 â\87\92 V2 & T1 â\87\92 T2 & U2 = ð\9d\95\94{Abst} V2. T2.
+fact tpr_inv_abst1_aux: â\88\80U1,U2. U1 â\9e¡ U2 â\86\92 â\88\80V1,T1. U1 = â\93\9bV1. T1 →
+                        â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93\9bV2. T2.
 #U1 #U2 * -U1 -U2
 [ #I #V #T #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
@@ -116,6 +116,6 @@ 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 →
-                     â\88\83â\88\83V2,T2. V1 â\87\92 V2 & T1 â\87\92 T2 & U2 = ð\9d\95\94{Abst} V2. T2.
+lemma tpr_inv_abst1: ∀V1,T1,U2. ⓛV1. T1 ➡ U2 →
+                     â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93\9bV2. T2.
 /2 width=3/ qed-.