hdiff
packages
feed
rzk
-0.11.4: test/typecheck/cases/ill-rstt-false-refl.rzk
#lang rzk-1 #set-option "rstt-safe" = "error" #def false-path (A : U) (a b : A) : a = b := refl