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