ill-data-eliminator-unknown.rzk

#lang rzk-1

-- An eliminate with clause must name one of the generated eliminators.
#data d := c
  eliminate with elim-d : (C : d → U) → C c → (x : d) → C x