-| lstas_succ: ∀G,L,K,W,V,U,i,l. ⬇[i] L ≡ K.ⓛW → lstas h l G K W V →
- ⬆[0, i+1] V ≡ U → lstas h (l+1) G L (#i) U
-| lstas_bind: ∀a,I,G,L,V,T,U,l. lstas h l G (L.ⓑ{I}V) T U →
- lstas h l G L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
-| lstas_appl: ∀G,L,V,T,U,l. lstas h l G L T U → lstas h l G L (ⓐV.T) (ⓐV.U)
-| lstas_cast: ∀G,L,W,T,U,l. lstas h l G L T U → lstas h l G L (ⓝW.T) U
+| lstas_succ: ∀G,L,K,W,V,U,i,d. ⬇[i] L ≡ K.ⓛW → lstas h d G K W V →
+ ⬆[0, i+1] V ≡ U → lstas h (d+1) G L (#i) U
+| lstas_bind: ∀a,I,G,L,V,T,U,d. lstas h d G (L.ⓑ{I}V) T U →
+ lstas h d G L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
+| lstas_appl: ∀G,L,V,T,U,d. lstas h d G L T U → lstas h d G L (ⓐV.T) (ⓐV.U)
+| lstas_cast: ∀G,L,W,T,U,d. lstas h d G L T U → lstas h d G L (ⓝW.T) U