-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. appl a n → cnv a h G L V → cnv a h G L T →
- â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0 â\86\92 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 →
- â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[1,h] U0 â\86\92 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 →
+ â\9dªG,Lâ\9d« â\8a¢ V â\9e¡*[1,h] W0 â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W0.U0 â\86\92 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 →
+ â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[1,h] U0 â\86\92 cnv h a G L (ⓝU.T)