ill-rstt-dependent-cube.rzk

#lang rzk-1

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