2
module IllegalUseOfIrrelevantDeclaration where
4
import Common.Irrelevance
6
record Subset (A : Set) (P : A -> Set) : Set where
13
.irrelevant : {A : Set} -> .A -> A
15
certificate : {A : Set}{P : A -> Set} -> (x : Subset A P) -> P (Subset.elem x)
16
certificate (a # p) = irrelevant p
b'\\ No newline at end of file'