-inductive snv (h) (g): relation3 genv lenv term ≝
-| snv_sort: ∀G,L,k. snv h g G L (⋆k)
-| snv_lref: â\88\80I,G,L,K,V,i. â¬\87[i] L â\89¡ K.â\93\91{I}V â\86\92 snv h g G K V â\86\92 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,W0,T,U0,l. snv h g G L V → snv h g G L T →
- ⦃G, L⦄ ⊢ V •*➡*[h, g, 1] W0 → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] ⓛ{a}W0.U0 → snv h g G L (ⓐV.T)
-| snv_cast: ∀G,L,U,T,U0. snv h g G L U → snv h g G L T →
- ⦃G, L⦄ ⊢ U •*➡*[h, g, 0] U0 → ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0 → snv h g G L (ⓝU.T)
+inductive snv (h) (o): relation3 genv lenv term ≝
+| snv_sort: ∀G,L,s. snv h o G L (⋆s)
+| snv_lref: â\88\80I,G,L,K,V,i. â¬\87[i] L â\89\98 K.â\93\91{I}V â\86\92 snv h o G K V â\86\92 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)