(* Basic properties *********************************************************)
+lemma tpss_strap1: ∀L,T1,T,T2,d,e.
+ L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
+/2 width=3/ qed.
+
lemma tpss_strap2: ∀L,T1,T,T2,d,e.
L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
/2 width=3/ qed.
lapply (tpss_weak_top … HT12) //
qed.
+lemma tpss_append: ∀K,T1,T2,d,e. K ⊢ T1 ▶* [d, e] T2 →
+ ∀L. L @@ K ⊢ T1 ▶* [d, e] T2.
+#K #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /3 width=3/
+qed.
+
(* Basic inversion lemmas ***************************************************)
(* Note: this can be derived from tpss_inv_atom1 *)
(* Basic forward lemmas *****************************************************)
-lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #[T1] ≤ #[T2].
+lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}.
#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT1
lapply (tps_fwd_tw … HT2) -HT2 #HT2