-inductive snv (h:sh) (g:sd h): lenv → predicate term ≝
-| snv_sort: ∀L,k. snv h g L (⋆k)
-| snv_lref: ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g K V → snv h g L (#i)
-| snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T)
-| snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T →
- ⦃G, L⦄ ⊢ V •[h, g] ⦃l+1, W⦄ → ⦃G, L⦄ ⊢ W ➡* W0 →
- ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
-| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
- ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ U ⬌* W → snv h g L (ⓝW.T)
+definition scast: ∀h. sd h → nat → relation4 genv lenv term term ≝
+ λh,g,l,G,L,V,W. ∀V0,W0,l0.
+ l0 ≤ l → ⦃G, L⦄ ⊢ V •*[h, l0+1] V0 → ⦃G, L⦄ ⊢ W •*[h, l0] W0 → ⦃G, L⦄ ⊢ V0 ⬌* W0.
+
+(* activate genv *)
+inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝
+| snv_sort: ∀G,L,k. snv h g G L (⋆k)
+| snv_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i)
+| snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T)
+| snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T →
+ ⦃G, L⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ V •[h] W → ⦃G, L⦄ ⊢ W ➡* W0 →
+ ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g G L (ⓐV.T)
+| snv_cast: ∀G,L,W,T,U,l. snv h g G L W → snv h g G L T →
+ ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ⬌* W → snv h g G L (ⓝW.T)