happy-rstt-boundary-error.rzk

#lang rzk-1

#set-option "rstt-safe" = "error"
#postulate overhang (f : (t : 2 | t === 0_2) → Unit [TOP ↦ unit]) : Unit