| 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_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)