warn-rstt-escape-unfolding.rzk

#lang rzk-1

-- Audit S2 alone: report both the introduction and its unfolded use.
#set-option "rstt-safe" = "off"
#set-option "warn-free-standing-restriction" = "yes"
#def restricted (A : U) (a : A) : U := A [TOP ↦ a]
#postulate use (A : U) (a : A) (x : restricted A a) : A