/2 width=8/ qed-.
(* Relocation properties ****************************************************)
(* Basic_1: was: subst1_lift_lt *)
lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
/2 width=8/ qed-.
(* Relocation properties ****************************************************)
(* Basic_1: was: subst1_lift_lt *)
lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →