-lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ →
- ∀L1. h ⊢ L1 ¡⊑[g] L2 →
- ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2.
+lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[h, g] ⦃l, U2⦄ →
+ ∀L1. h ⊢ L1 ¡⊑[h, g] L2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T •[h, g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2.