2
module IrrelevantDeclaration 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