rzk-0.8.0: test/typecheck/cases/ill-tope-subtle-tope-family-5d.expect.yaml

status: error
error_tag: TypeErrorTopeNotSatisfied
message_contains:
  - "unifying"
  - "does not entail"
  - "π₁"
regression_for:
  - tope-family-5d-without-local-Phi