ill-data-eliminator-mismatch.expect.yaml

status: error
error_tag: TypeErrorReascribedTypeMismatch
message_contains:
  - "the re-ascribed type of ind-d"
  - "is not definitionally equal to its canonical type"
  - "(C : d → U) → C c → (x : d) → C x"
line: 5
regression_for:
  - data-eliminator-reascription-clause