now looks like the other refinements for local environments
14 files changed:
(* Note: it does not hold replacing |L1| with |L2| *)
lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
(* Note: it does not hold replacing |L1| with |L2| *)
lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
- â\88\80L2. L2 â\89¼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
+ â\88\80L2. L2 â\8a\91 [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/
qed-.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/
qed-.
-lemma lsubsv_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 ¡â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L1|] L2.
+lemma lsubsv_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 ¡â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L1|] L2.
/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr1/
qed-.
/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr1/
qed-.
-lemma lsubsv_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 ¡â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L2|] L2.
+lemma lsubsv_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 ¡â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L2|] L2.
/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr2/
qed-.
/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubr2/
qed-.
(* Note: it does not hold replacing |L1| with |L2| *)
lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
(* Note: it does not hold replacing |L1| with |L2| *)
lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
- â\88\80L2. L2 â\89¼ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
+ â\88\80L2. L2 â\8a\91 [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
#L1 #T1 #T2 #HT12
elim (cpcs_inv_cprs … HT12) -HT12
/3 width=5 by cprs_div, cprs_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *)
#L1 #T1 #T2 #HT12
elim (cpcs_inv_cprs … HT12) -HT12
/3 width=5 by cprs_div, cprs_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *)
(* Basic_forward lemmas *****************************************************)
(* Basic_forward lemmas *****************************************************)
-lemma lsubss_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L1|] L2.
+lemma lsubss_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L1|] L2.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.
-lemma lsubss_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L2|] L2.
+lemma lsubss_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L2|] L2.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
-notation "hvbox( T1 break â\89¼ [ term 46 d , break term 46 e ] break term 46 T2 )"
+notation "hvbox( T1 break â\8a\91 [ term 46 d , break term 46 e ] break term 46 T2 )"
non associative with precedence 45
for @{ 'SubEq $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'SubEq $T1 $d $e $T2 }.
(* Note: it does not hold replacing |L1| with |L2| *)
(* Basic_1: was only: pr2_change *)
lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
(* Note: it does not hold replacing |L1| with |L2| *)
(* Basic_1: was only: pr2_change *)
lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
- â\88\80L2. L2 â\89¼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
+ â\88\80L2. L2 â\8a\91 [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
qed.
#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
qed.
-lemma ldrop_lsubr_ldrop2_abbr: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+lemma ldrop_lsubr_ldrop2_abbr: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
d ≤ i → i < d + e →
∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →
d ≤ i → i < d + e →
- â\88\83â\88\83K1. K1 â\89¼ [0, d + e - i - 1] K2 &
+ â\88\83â\88\83K1. K1 â\8a\91 [0, d + e - i - 1] K2 &
⇩[0, i] L1 ≡ K1. ⓓV.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
[ #d #e #K1 #V #i #H
⇩[0, i] L1 ≡ K1. ⓓV.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
[ #d #e #K1 #V #i #H
definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
∀L2,s1,s2. R L2 s1 s2 →
definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R.
∀L2,s1,s2. R L2 s1 s2 →
- â\88\80L1,d,e. L1 â\89¼ [d, e] L2 → R L1 s1 s2.
+ â\88\80L1,d,e. L1 â\8a\91 [d, e] L2 → R L1 s1 s2.
(* Basic properties *********************************************************)
(* Basic properties *********************************************************)
-lemma lsubr_bind_eq: â\88\80L1,L2,e. L1 â\89¼ [0, e] L2 → ∀I,V.
- L1. â\93\91{I} V â\89¼ [0, e + 1] L2.ⓑ{I} V.
+lemma lsubr_bind_eq: â\88\80L1,L2,e. L1 â\8a\91 [0, e] L2 → ∀I,V.
+ L1. â\93\91{I} V â\8a\91 [0, e + 1] L2.ⓑ{I} V.
#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
qed.
#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
qed.
-lemma lsubr_abbr_lt: â\88\80L1,L2,V,e. L1 â\89¼ [0, e - 1] L2 → 0 < e →
- L1. â\93\93V â\89¼ [0, e] L2.ⓓV.
+lemma lsubr_abbr_lt: â\88\80L1,L2,V,e. L1 â\8a\91 [0, e - 1] L2 → 0 < e →
+ L1. â\93\93V â\8a\91 [0, e] L2.ⓓV.
#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
-lemma lsubr_abst_lt: â\88\80L1,L2,I,V1,V2,e. L1 â\89¼ [0, e - 1] L2 → 0 < e →
- L1. â\93\91{I}V1 â\89¼ [0, e] L2. ⓛV2.
+lemma lsubr_abst_lt: â\88\80L1,L2,I,V1,V2,e. L1 â\8a\91 [0, e - 1] L2 → 0 < e →
+ L1. â\93\91{I}V1 â\8a\91 [0, e] L2. ⓛV2.
#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
-lemma lsubr_skip_lt: â\88\80L1,L2,d,e. L1 â\89¼ [d - 1, e] L2 → 0 < d →
- â\88\80I1,I2,V1,V2. L1. â\93\91{I1} V1 â\89¼ [d, e] L2. ⓑ{I2} V2.
+lemma lsubr_skip_lt: â\88\80L1,L2,d,e. L1 â\8a\91 [d - 1, e] L2 → 0 < d →
+ â\88\80I1,I2,V1,V2. L1. â\93\91{I1} V1 â\8a\91 [d, e] L2. ⓑ{I2} V2.
#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
qed.
#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
qed.
-lemma lsubr_bind_lt: â\88\80I,L1,L2,V,e. L1 â\89¼ [0, e - 1] L2 → 0 < e →
- L1. â\93\93V â\89¼ [0, e] L2. ⓑ{I}V.
+lemma lsubr_bind_lt: â\88\80I,L1,L2,V,e. L1 â\8a\91 [0, e - 1] L2 → 0 < e →
+ L1. â\93\93V â\8a\91 [0, e] L2. ⓑ{I}V.
-lemma lsubr_refl: â\88\80d,e,L. L â\89¼ [d, e] L.
+lemma lsubr_refl: â\88\80d,e,L. L â\8a\91 [d, e] L.
#d elim d -d
[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
| #d #IHd #e #L elim L -L // /2 width=1/
#d elim d -d
[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
| #d #IHd #e #L elim L -L // /2 width=1/
(* Basic inversion lemmas ***************************************************)
(* Basic inversion lemmas ***************************************************)
-fact lsubr_inv_atom1_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 → L1 = ⋆ →
+fact lsubr_inv_atom1_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 → L1 = ⋆ →
L2 = ⋆ ∨ (d = 0 ∧ e = 0).
#L1 #L2 #d #e * -L1 -L2 -d -e
[ /2 width=1/
L2 = ⋆ ∨ (d = 0 ∧ e = 0).
#L1 #L2 #d #e * -L1 -L2 -d -e
[ /2 width=1/
-lemma lsubr_inv_atom1: â\88\80L2,d,e. â\8b\86 â\89¼ [d, e] L2 →
+lemma lsubr_inv_atom1: â\88\80L2,d,e. â\8b\86 â\8a\91 [d, e] L2 →
L2 = ⋆ ∨ (d = 0 ∧ e = 0).
/2 width=3/ qed-.
L2 = ⋆ ∨ (d = 0 ∧ e = 0).
/2 width=3/ qed-.
-fact lsubr_inv_skip1_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_inv_skip1_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
- â\88\83â\88\83I2,K2,V2. K1 â\89¼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+ â\88\83â\88\83I2,K2,V2. K1 â\8a\91 [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #I1 #K1 #V1 #H destruct
| #L1 #L2 #I1 #K1 #V1 #_ #H
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #I1 #K1 #V1 #H destruct
| #L1 #L2 #I1 #K1 #V1 #_ #H
-lemma lsubr_inv_skip1: â\88\80I1,K1,L2,V1,d,e. K1.â\93\91{I1}V1 â\89¼ [d, e] L2 → 0 < d →
- â\88\83â\88\83I2,K2,V2. K1 â\89¼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+lemma lsubr_inv_skip1: â\88\80I1,K1,L2,V1,d,e. K1.â\93\91{I1}V1 â\8a\91 [d, e] L2 → 0 < d →
+ â\88\83â\88\83I2,K2,V2. K1 â\8a\91 [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
-fact lsubr_inv_atom2_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 → L2 = ⋆ →
+fact lsubr_inv_atom2_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 → L2 = ⋆ →
L1 = ⋆ ∨ (d = 0 ∧ e = 0).
#L1 #L2 #d #e * -L1 -L2 -d -e
[ /2 width=1/
L1 = ⋆ ∨ (d = 0 ∧ e = 0).
#L1 #L2 #d #e * -L1 -L2 -d -e
[ /2 width=1/
-lemma lsubr_inv_atom2: â\88\80L1,d,e. L1 â\89¼ [d, e] ⋆ →
+lemma lsubr_inv_atom2: â\88\80L1,d,e. L1 â\8a\91 [d, e] ⋆ →
L1 = ⋆ ∨ (d = 0 ∧ e = 0).
/2 width=3/ qed-.
L1 = ⋆ ∨ (d = 0 ∧ e = 0).
/2 width=3/ qed-.
-fact lsubr_inv_abbr2_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_inv_abbr2_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
- â\88\83â\88\83K1. K1 â\89¼ [0, e - 1] K2 & L1 = K1.ⓓV.
+ â\88\83â\88\83K1. K1 â\8a\91 [0, e - 1] K2 & L1 = K1.ⓓV.
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #K1 #V #H destruct
| #L1 #L2 #K1 #V #_ #_ #H
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #K1 #V #H destruct
| #L1 #L2 #K1 #V #_ #_ #H
-lemma lsubr_inv_abbr2: â\88\80L1,K2,V,e. L1 â\89¼ [0, e] K2.ⓓV → 0 < e →
- â\88\83â\88\83K1. K1 â\89¼ [0, e - 1] K2 & L1 = K1.ⓓV.
+lemma lsubr_inv_abbr2: â\88\80L1,K2,V,e. L1 â\8a\91 [0, e] K2.ⓓV → 0 < e →
+ â\88\83â\88\83K1. K1 â\8a\91 [0, e - 1] K2 & L1 = K1.ⓓV.
-fact lsubr_inv_skip2_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_inv_skip2_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
- â\88\83â\88\83I1,K1,V1. K1 â\89¼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
+ â\88\83â\88\83I1,K1,V1. K1 â\8a\91 [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #I1 #K1 #V1 #H destruct
| #L1 #L2 #I1 #K1 #V1 #_ #H
#L1 #L2 #d #e * -L1 -L2 -d -e
[ #d #e #I1 #K1 #V1 #H destruct
| #L1 #L2 #I1 #K1 #V1 #_ #H
-lemma lsubr_inv_skip2: â\88\80I2,L1,K2,V2,d,e. L1 â\89¼ [d, e] K2.ⓑ{I2}V2 → 0 < d →
- â\88\83â\88\83I1,K1,V1. K1 â\89¼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
+lemma lsubr_inv_skip2: â\88\80I2,L1,K2,V2,d,e. L1 â\8a\91 [d, e] K2.ⓑ{I2}V2 → 0 < d →
+ â\88\83â\88\83I1,K1,V1. K1 â\8a\91 [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
/2 width=5/ qed-.
(* Basic forward lemmas *****************************************************)
/2 width=5/ qed-.
(* Basic forward lemmas *****************************************************)
-fact lsubr_fwd_length_full1_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_fwd_length_full1_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
d = 0 → e = |L1| → |L1| ≤ |L2|.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
[ //
d = 0 → e = |L1| → |L1| ≤ |L2|.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
[ //
-lemma lsubr_fwd_length_full1: â\88\80L1,L2. L1 â\89¼ [0, |L1|] L2 → |L1| ≤ |L2|.
+lemma lsubr_fwd_length_full1: â\88\80L1,L2. L1 â\8a\91 [0, |L1|] L2 → |L1| ≤ |L2|.
-fact lsubr_fwd_length_full2_aux: â\88\80L1,L2,d,e. L1 â\89¼ [d, e] L2 →
+fact lsubr_fwd_length_full2_aux: â\88\80L1,L2,d,e. L1 â\8a\91 [d, e] L2 →
d = 0 → e = |L2| → |L2| ≤ |L1|.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
[ //
d = 0 → e = |L2| → |L2| ≤ |L1|.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
[ //
-lemma lsubr_fwd_length_full2: â\88\80L1,L2. L1 â\89¼ [0, |L2|] L2 → |L2| ≤ |L1|.
+lemma lsubr_fwd_length_full2: â\88\80L1,L2. L1 â\8a\91 [0, |L2|] L2 → |L2| ≤ |L1|.
(* Basic properties *********************************************************)
lemma tps_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
(* Basic properties *********************************************************)
lemma tps_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
- â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ T1 ▶ [d, e] T2.
+ â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ T1 ▶ [d, e] T2.
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
[ //
| #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
[ //
| #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
/2 width=3/ qed.
lemma delift_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 →
/2 width=3/ qed.
lemma delift_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 →
- â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2.
+ â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2.
#L1 #T1 #T2 #d #e * /3 width=3/
qed.
#L1 #T1 #T2 #d #e * /3 width=3/
qed.
(* Basic properties *********************************************************)
lemma delifta_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
(* Basic properties *********************************************************)
lemma delifta_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
- â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
+ â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
[ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
[ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
/2 width=3/ qed.
lemma tpss_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
/2 width=3/ qed.
lemma tpss_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
- â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
+ â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
/3 width=3/ qed.
lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T.
/3 width=3/ qed.
lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T.
(* Basic properties *********************************************************)
lemma tpssa_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
(* Basic properties *********************************************************)
lemma tpssa_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
- â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
+ â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
[ //
| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
[ //
| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
}
]
[ { "local env. ref. for substitution" * } {
}
]
[ { "local env. ref. for substitution" * } {
- [ "lsubr ( ? â\89¼[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ]
+ [ "lsubr ( ? â\8a\91[?,?] ? )" "(lsubr_lsubr)" "lsubr_sfr ( ≽[?,?] ? )" * ]
}
]
[ { "restricted structural predecessor for closures" * } {
}
]
[ { "restricted structural predecessor for closures" * } {