(* Relocation properties ****************************************************)
(* Basic_1: was: pr0_lift *)
-lemma tpr_lift: â\88\80T1,T2. T1 â\87\92 T2 →
- â\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.
+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
qed.
(* Basic_1: was: pr0_gen_lift *)
-lemma tpr_inv_lift: â\88\80T1,T2. T1 â\87\92 T2 →
- â\88\80d,e,U1. â\87\91[d, e] U1 ≡ T1 →
- â\88\83â\88\83U2. â\87\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/
(* 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
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-.