- support for candidates of reducibility continues ...

[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..32a80aafc83c7e74ef166e42d7a0d6a846481510 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
@@ -21,7 +21,7 @@ include "Basic_2/reducibility/tpr.ma".
 
 (* Basic_1: was: pr0_lift *)
 lemma tpr_lift: ∀T1,T2. T1 ⇒ 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.
+                â\88\80d,e,U1. â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92 U1 â\87\92 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 →
-                    â\88\80d,e,U1. â\86\91[d, e] U1 â\89¡ T1 â\86\92
-                    â\88\83â\88\83U2. â\86\91[d, e] U2 â\89¡ T2 & U1 â\87\92 U2.
+                    â\88\80d,e,U1. â\87\91[d, e] U1 â\89¡ T1 â\86\92
+                    â\88\83â\88\83U2. â\87\91[d, e] U2 â\89¡ T2 & U1 â\87\92 U2.
 #T1 #T2 #H elim H -T1 -T2
 [ * #i #d #e #U1 #HU1
   [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/