-lemma lsubsv_lstas_trans: ∀h,g,G,L2,T,U2,d2. ⦃G, L2⦄ ⊢ T •*[h, d2] U2 →
- ∀d1. d2 ≤ d1 → ⦃G, L2⦄ ⊢ T ▪[h, g] d1 →
- ∀L1. G ⊢ L1 ⫃¡[h, g] L2 →
+lemma lsubsv_lstas_trans: ∀h,o,G,L2,T,U2,d2. ⦃G, L2⦄ ⊢ T •*[h, d2] U2 →
+ ∀d1. d2 ≤ d1 → ⦃G, L2⦄ ⊢ T ▪[h, o] d1 →
+ ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →