tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
-| tpr_tau : â\88\80V,T1,T2. tpr T1 T2 â\86\92 tpr (â\93£V. T1) T2
+| tpr_tau : â\88\80V,T1,T2. tpr T1 T2 â\86\92 tpr (â\93\9dV. T1) T2
.
interpretation
qed-.
(* Note: the main property of simple terms *)
-lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒[T1] →
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
U = ⓐV2. T2.
#V1 #T1 #U #H #HT1
qed-.
(* Basic_1: was: pr0_gen_cast *)
-lemma tpr_inv_cast1: â\88\80V1,T1,U2. â\93£V1. T1 ➡ U2 →
- (â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93£V2. T2)
+lemma tpr_inv_cast1: â\88\80V1,T1,U2. â\93\9dV1. T1 ➡ U2 →
+ (â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93\9dV2. T2)
∨ T1 ➡ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_flat1 … H) -H * /3 width=5/
∨∨ T1 = #i
| ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
T1 = ⓓV. T
- | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93£V. T.
+ | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93\9dV. T.
#T1 #T2 * -T1 -T2
[ #I #i #H destruct /2 width=1/
| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
∨∨ T1 = #i
| ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
T1 = ⓓV. T
- | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93£V. T.
+ | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93\9dV. T.
/2 width=3/ qed-.
(* Basic_1: removed theorems 3: