-inductive cnv (a) (h): relation3 genv lenv term ≝
-| cnv_sort: ∀G,L,s. cnv a h G L (⋆s)
-| cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0)
-| cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i)
-| cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T)
-| cnv_appl: ∀n,p,G,L,V,W0,T,U0. (a = Ⓣ → n ≤ 1) → cnv a h G L V → cnv a h G L T →
- ⦃G, L⦄ ⊢ V ➡*[1, h] W0 → ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0 → cnv a h G L (ⓐV.T)
-| cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T →
- ⦃G, L⦄ ⊢ U ➡*[h] U0 → ⦃G, L⦄ ⊢ T ➡*[1, h] U0 → cnv a h G L (ⓝU.T)
+inductive cnv (h) (a): relation3 genv lenv term ≝
+| cnv_sort: ∀G,L,s. cnv h a G L (⋆s)
+| cnv_zero: ∀I,G,K,V. cnv h a G K V → cnv h a G (K.ⓑ{I}V) (#0)
+| cnv_lref: ∀I,G,K,i. cnv h a G K (#i) → cnv h a G (K.ⓘ{I}) (#↑i)
+| cnv_bind: ∀p,I,G,L,V,T. cnv h a G L V → cnv h a G (L.ⓑ{I}V) T → cnv h a G L (ⓑ{p,I}V.T)
+| cnv_appl: ∀n,p,G,L,V,W0,T,U0. ad a n → cnv h a G L V → cnv h a G L T →
+ ⦃G,L⦄ ⊢ V ➡*[1,h] W0 → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0 → cnv h a G L (ⓐV.T)
+| cnv_cast: ∀G,L,U,T,U0. cnv h a G L U → cnv h a G L T →
+ ⦃G,L⦄ ⊢ U ➡*[h] U0 → ⦃G,L⦄ ⊢ T ➡*[1,h] U0 → cnv h a G L (ⓝU.T)