warn-rstt-escape-beta.rzk

#lang rzk-1

-- Audit S2 alone: report the introduction, not an unfolded use site.
#set-option "rstt-safe" = "off"
#set-option "warn-free-standing-restriction" = "yes"
#def beta (A : U) (a : A) : U := (\ (X : U) → X) (A [TOP ↦ a])