Not : Type -> Type
Not t = t -> Void
public export

  uninhabited : t -> Void

  uninhabited : Not t

  Yes : (prf : prop)         -> Dec prop
  No  : (ctr : prop -> Void) -> Dec prop

  Yes : (prf : p)     -> Dec p
  No  : (ctr : Not p) -> Dec p