-fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →
- ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
- ∃∃K1,V1. K1 [0, e - 1] ≫ K2 &
- K2 ⊢ V1 [0, e - 1] ≫ V2 &
- L1 = K1. 𝕓{I} V1.
+lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶* ⋆ → L1 = ⋆.
+/2 width=5/ qed-.
+(*
+fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
+ ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 [0, e - 1] ▶ K2 &
+ K2 ⊢ V1 [0, e - 1] ▶ V2 &
+ L1 = K1. ⓑ{I} V1.