-| da_sort: ∀G,L,k,l. deg h g k l → da h g G L (⋆k) l
-| da_ldef: ∀G,L,K,V,i,l. ⬇[i] L ≡ K.ⓓV → da h g G K V l → da h g G L (#i) l
-| da_ldec: ∀G,L,K,W,i,l. ⬇[i] L ≡ K.ⓛW → da h g G K W l → da h g G L (#i) (l+1)
-| da_bind: ∀a,I,G,L,V,T,l. da h g G (L.ⓑ{I}V) T l → da h g G L (ⓑ{a,I}V.T) l
-| da_flat: ∀I,G,L,V,T,l. da h g G L T l → da h g G L (ⓕ{I}V.T) l
+| da_sort: ∀G,L,k,d. deg h g k d → da h g G L (⋆k) d
+| da_ldef: ∀G,L,K,V,i,d. ⬇[i] L ≡ K.ⓓV → da h g G K V d → da h g G L (#i) d
+| da_ldec: ∀G,L,K,W,i,d. ⬇[i] L ≡ K.ⓛW → da h g G K W d → da h g G L (#i) (d+1)
+| da_bind: ∀a,I,G,L,V,T,d. da h g G (L.ⓑ{I}V) T d → da h g G L (ⓑ{a,I}V.T) d
+| da_flat: ∀I,G,L,V,T,d. da h g G L T d → da h g G L (ⓕ{I}V.T) d