inductive tps: nat → nat → lenv → relation term ≝
| tps_atom : ∀L,I,d,e. tps d e L (𝕒{I}) (𝕒{I})
| tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
inductive tps: nat → nat → lenv → relation term ≝
| tps_atom : ∀L,I,d,e. tps d e L (𝕒{I}) (𝕒{I})
| tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
| tps_bind : ∀L,I,V1,V2,T1,T2,d,e.
tps d e L V1 V2 → tps (d + 1) e (L. 𝕓{I} V2) T1 T2 →
tps d e L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
| tps_bind : ∀L,I,V1,V2,T1,T2,d,e.
tps d e L V1 V2 → tps (d + 1) e (L. 𝕓{I} V2) T1 T2 →
tps d e L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
-lemma tps_lsubs_conf: â\88\80L1,T1,T2,d,e. L1 â\8a¢ T1 [d, e] â\89« T2 →
- â\88\80L2. L1 [d, e] â\89¼ L2 â\86\92 L2 â\8a¢ T1 [d, e] â\89« T2.
+lemma tps_lsubs_conf: â\88\80L1,T1,T2,d,e. L1 â\8a¢ T1 [d, e] â\96¶ T2 →
+ â\88\80L2. L1 [d, e] â\89¼ L2 â\86\92 L2 â\8a¢ T1 [d, e] â\96¶ 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
-lemma tps_refl: â\88\80T,L,d,e. L â\8a¢ T [d, e] â\89« T.
+lemma tps_refl: â\88\80T,L,d,e. L â\8a¢ T [d, e] â\96¶ T.
-lemma tps_full: â\88\80K,V,T1,L,d. â\87\93[0, d] L ≡ (K. 𝕓{Abbr} V) →
- â\88\83â\88\83T2,T. L â\8a¢ T1 [d, 1] â\89« T2 & â\87\91[d, 1] T ≡ T2.
+lemma tps_full: â\88\80K,V,T1,L,d. â\87©[0, d] L ≡ (K. 𝕓{Abbr} V) →
+ â\88\83â\88\83T2,T. L â\8a¢ T1 [d, 1] â\96¶ T2 & â\87§[d, 1] T ≡ T2.
-lemma tps_weak: â\88\80L,T1,T2,d1,e1. L â\8a¢ T1 [d1, e1] â\89« T2 →
+lemma tps_weak: â\88\80L,T1,T2,d1,e1. L â\8a¢ T1 [d1, e1] â\96¶ T2 →
#L #T1 #T2 #d1 #e1 #H elim H -L -T1 -T2 -d1 -e1
[ //
| #L #K #V #W #i #d1 #e1 #Hid1 #Hide1 #HLK #HVW #d2 #e2 #Hd12 #Hde12
#L #T1 #T2 #d1 #e1 #H elim H -L -T1 -T2 -d1 -e1
[ //
| #L #K #V #W #i #d1 #e1 #Hid1 #Hide1 #HLK #HVW #d2 #e2 #Hd12 #Hde12
qed.
lemma tps_weak_top: ∀L,T1,T2,d,e.
qed.
lemma tps_weak_top: ∀L,T1,T2,d,e.
qed.
lemma tps_weak_all: ∀L,T1,T2,d,e.
qed.
lemma tps_weak_all: ∀L,T1,T2,d,e.
-lemma tps_split_up: â\88\80L,T1,T2,d,e. L â\8a¢ T1 [d, e] â\89« T2 → ∀i. d ≤ i → i ≤ d + e →
- â\88\83â\88\83T. L â\8a¢ T1 [d, i - d] â\89« T & L â\8a¢ T [i, d + e - i] â\89« T2.
+lemma tps_split_up: â\88\80L,T1,T2,d,e. L â\8a¢ T1 [d, e] â\96¶ T2 → ∀i. d ≤ i → i ≤ d + e →
+ â\88\83â\88\83T. L â\8a¢ T1 [d, i - d] â\96¶ T & L â\8a¢ T [i, d + e - i] â\96¶ T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
[ /2 width=3/
| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
[ /2 width=3/
| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
-fact tps_inv_atom1_aux: â\88\80L,T1,T2,d,e. L â\8a¢ T1 [d, e] â\89« T2 → ∀I. T1 = 𝕒{I} →
+fact tps_inv_atom1_aux: â\88\80L,T1,T2,d,e. L â\8a¢ T1 [d, e] â\96¶ T2 → ∀I. T1 = 𝕒{I} →
- â\87\93[O, i] L ≡ K. 𝕓{Abbr} V &
- â\87\91[O, i + 1] V ≡ T2 &
+ â\87©[O, i] L ≡ K. 𝕓{Abbr} V &
+ â\87§[O, i + 1] V ≡ T2 &
-lemma tps_inv_atom1: â\88\80L,T2,I,d,e. L â\8a¢ ð\9d\95\92{I} [d, e] â\89« T2 →
+lemma tps_inv_atom1: â\88\80L,T2,I,d,e. L â\8a¢ ð\9d\95\92{I} [d, e] â\96¶ T2 →
- â\87\93[O, i] L ≡ K. 𝕓{Abbr} V &
- â\87\91[O, i + 1] V ≡ T2 &
+ â\87©[O, i] L ≡ K. 𝕓{Abbr} V &
+ â\87§[O, i + 1] V ≡ T2 &
-lemma tps_inv_sort1: â\88\80L,T2,k,d,e. L â\8a¢ â\8b\86k [d, e] â\89« T2 → T2 = ⋆k.
+lemma tps_inv_sort1: â\88\80L,T2,k,d,e. L â\8a¢ â\8b\86k [d, e] â\96¶ T2 → T2 = ⋆k.
#L #T2 #k #d #e #H
elim (tps_inv_atom1 … H) -H //
* #K #V #i #_ #_ #_ #_ #H destruct
qed-.
(* Basic_1: was: subst1_gen_lref *)
#L #T2 #k #d #e #H
elim (tps_inv_atom1 … H) -H //
* #K #V #i #_ #_ #_ #_ #H destruct
qed-.
(* Basic_1: was: subst1_gen_lref *)
-lemma tps_inv_lref1: â\88\80L,T2,i,d,e. L â\8a¢ #i [d, e] â\89« T2 →
+lemma tps_inv_lref1: â\88\80L,T2,i,d,e. L â\8a¢ #i [d, e] â\96¶ T2 →
- â\87\93[O, i] L ≡ K. 𝕓{Abbr} V &
- â\87\91[O, i + 1] V ≡ T2.
+ â\87©[O, i] L ≡ K. 𝕓{Abbr} V &
+ â\87§[O, i + 1] V ≡ T2.
-lemma tps_inv_gref1: â\88\80L,T2,p,d,e. L â\8a¢ §p [d, e] â\89« T2 → T2 = §p.
+lemma tps_inv_gref1: â\88\80L,T2,p,d,e. L â\8a¢ §p [d, e] â\96¶ T2 → T2 = §p.
-fact tps_inv_bind1_aux: â\88\80d,e,L,U1,U2. L â\8a¢ U1 [d, e] â\89« U2 →
+fact tps_inv_bind1_aux: â\88\80d,e,L,U1,U2. L â\8a¢ U1 [d, e] â\96¶ U2 →
- â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\89« V2 &
- L. ð\9d\95\93{I} V2 â\8a¢ T1 [d + 1, e] â\89« T2 &
+ â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\96¶ V2 &
+ L. ð\9d\95\93{I} V2 â\8a¢ T1 [d + 1, e] â\96¶ T2 &
-lemma tps_inv_bind1: â\88\80d,e,L,I,V1,T1,U2. L â\8a¢ ð\9d\95\93{I} V1. T1 [d, e] â\89« U2 →
- â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\89« V2 &
- L. ð\9d\95\93{I} V2 â\8a¢ T1 [d + 1, e] â\89« T2 &
+lemma tps_inv_bind1: â\88\80d,e,L,I,V1,T1,U2. L â\8a¢ ð\9d\95\93{I} V1. T1 [d, e] â\96¶ U2 →
+ â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\96¶ V2 &
+ L. ð\9d\95\93{I} V2 â\8a¢ T1 [d + 1, e] â\96¶ T2 &
-fact tps_inv_flat1_aux: â\88\80d,e,L,U1,U2. L â\8a¢ U1 [d, e] â\89« U2 →
+fact tps_inv_flat1_aux: â\88\80d,e,L,U1,U2. L â\8a¢ U1 [d, e] â\96¶ U2 →
- â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\89« V2 & L â\8a¢ T1 [d, e] â\89« T2 &
+ â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\96¶ V2 & L â\8a¢ T1 [d, e] â\96¶ T2 &
-lemma tps_inv_flat1: â\88\80d,e,L,I,V1,T1,U2. L â\8a¢ ð\9d\95\97{I} V1. T1 [d, e] â\89« U2 →
- â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\89« V2 & L â\8a¢ T1 [d, e] â\89« T2 &
+lemma tps_inv_flat1: â\88\80d,e,L,I,V1,T1,U2. L â\8a¢ ð\9d\95\97{I} V1. T1 [d, e] â\96¶ U2 →
+ â\88\83â\88\83V2,T2. L â\8a¢ V1 [d, e] â\96¶ V2 & L â\8a¢ T1 [d, e] â\96¶ T2 &
-fact tps_inv_refl_O2_aux: â\88\80L,T1,T2,d,e. L â\8a¢ T1 [d, e] â\89« T2 → e = 0 → T1 = T2.
+fact tps_inv_refl_O2_aux: â\88\80L,T1,T2,d,e. L â\8a¢ T1 [d, e] â\96¶ T2 → e = 0 → T1 = T2.
-lemma tps_inv_refl_O2: â\88\80L,T1,T2,d. L â\8a¢ T1 [d, 0] â\89« T2 → T1 = T2.
+lemma tps_inv_refl_O2: â\88\80L,T1,T2,d. L â\8a¢ T1 [d, 0] â\96¶ T2 → T1 = T2.
-lemma tps_fwd_tw: â\88\80L,T1,T2,d,e. L â\8a¢ T1 [d, e] â\89« T2 → #[T1] ≤ #[T2].
+lemma tps_fwd_tw: â\88\80L,T1,T2,d,e. L â\8a¢ T1 [d, e] â\96¶ T2 → #[T1] ≤ #[T2].
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e normalize
/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
qed-.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e normalize
/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
qed-.