-inductive ssta (h:sh) (g:sd h): nat → lenv → relation term ≝
-| ssta_sort: ∀L,k,l. deg h g k l → ssta h g l L (⋆k) (⋆(next h k))
-| ssta_ldef: ∀L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l K V W →
- ⇧[0, i + 1] W ≡ U → ssta h g l L (#i) U
-| ssta_ldec: ∀L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → ssta h g l K W V →
- ⇧[0, i + 1] W ≡ U → ssta h g (l+1) L (#i) U
-| ssta_bind: ∀a,I,L,V,T,U,l. ssta h g l (L. ⓑ{I} V) T U →
- ssta h g l L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
-| ssta_appl: ∀L,V,T,U,l. ssta h g l L T U →
- ssta h g l L (ⓐV.T) (ⓐV.U)
-| ssta_cast: ∀L,W,T,U,l. ssta h g l L T U → ssta h g l L (ⓝW. T) U
+(* activate genv *)
+inductive ssta (h:sh) (g:sd h): nat → genv → lenv → relation term ≝
+| ssta_sort: ∀G,L,k,l. deg h g k l → ssta h g l G L (⋆k) (⋆(next h k))
+| ssta_ldef: ∀G,L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l G K V W →
+ ⇧[0, i + 1] W ≡ U → ssta h g l G L (#i) U
+| ssta_ldec: ∀G,L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → ssta h g l G K W V →
+ ⇧[0, i + 1] W ≡ U → ssta h g (l+1) G L (#i) U
+| ssta_bind: ∀a,I,G,L,V,T,U,l. ssta h g l G (L. ⓑ{I} V) T U →
+ ssta h g l G L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
+| ssta_appl: ∀G,L,V,T,U,l. ssta h g l G L T U →
+ ssta h g l G L (ⓐV.T) (ⓐV.U)
+| ssta_cast: ∀G,L,W,T,U,l. ssta h g l G L T U → ssta h g l G L (ⓝW.T) U