-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 →
- ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
- ⦃h, L⦄ ⊢ T •*➡*[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 →
- ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T)
+(* activate genv *)
+inductive snv (h) (o): relation3 genv lenv term ≝
+| snv_sort: ∀G,L,s. snv h o G L (⋆s)
+| snv_lref: ∀I,G,L,K,V,i. ⬇[i] L ≘ K.ⓑ{I}V → snv h o G K V → snv h o G L (#i)
+| snv_bind: ∀a,I,G,L,V,T. snv h o G L V → snv h o G (L.ⓑ{I}V) T → snv h o G L (ⓑ{a,I}V.T)
+| snv_appl: ∀a,G,L,V,W0,T,U0,d. snv h o G L V → snv h o G L T →
+ ⦃G, L⦄ ⊢ V •*➡*[h, o, 1] W0 → ⦃G, L⦄ ⊢ T •*➡*[h, o, d] ⓛ{a}W0.U0 → snv h o G L (ⓐV.T)
+| snv_cast: ∀G,L,U,T,U0. snv h o G L U → snv h o G L T →
+ ⦃G, L⦄ ⊢ U •*➡*[h, o, 0] U0 → ⦃G, L⦄ ⊢ T •*➡*[h, o, 1] U0 → snv h o G L (ⓝU.T)