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