Dependent lists

[anuyts]

This is not the primary thing that the cubical library was missing, but I needed them so why not contribute :-)
In the near future, I'm likely to make more contributions of similar nature.

[xekoukou]

I think, this can be abstracted to heterogeneous lists, like in idris.

HVEC

[anuyts]

I would say heterogeneous lists are a special case, where B is the identity.

[ecavallo]

Looks good, thanks!