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