ill-rstt-dependent-cube-family.rzk

#lang rzk-1

#set-option "rstt-safe" = "error"
#def dependent (I : 2 → CUBE) (s : 2)
  (A : (t : I s) → U) : Unit := unit