rzk-0.11.4: test/typecheck/cases/ill-rstt-restriction-in-domain.rzk
#lang rzk-1 #set-option "rstt-safe" = "error" #def missed (A : U) (a : A) : (t : 2 | ((\ (x : A [TOP ↦ a]) → 0_2) a) === 0_2) → A := \ t → a
#lang rzk-1 #set-option "rstt-safe" = "error" #def missed (A : U) (a : A) : (t : 2 | ((\ (x : A [TOP ↦ a]) → 0_2) a) === 0_2) → A := \ t → a