rzk-0.11.4: test/typecheck/cases/ill-data-cube-universe-index.rzk
#lang rzk-1 -- An index must be a type, full stop: a family over the cube universe is -- internal quantification over the cube layer. #data X : CUBE -> U
#lang rzk-1 -- An index must be a type, full stop: a family over the cube universe is -- internal quantification over the cube layer. #data X : CUBE -> U