happy-rstt-boundary-warn.rzk

#lang rzk-1

-- Boundary obligations are interpreted within the binder's shape.
#postulate overhang (f : (t : 2 | t === 0_2) → Unit [TOP ↦ unit]) : Unit