[Agda] excluded-middle

[Nils Anders Danielsson]

On 2016-06-22 03:59, Katsutoshi Itoh wrote:
> 3. double negate elimination is valid in the logic

No, it's not.

> I've beleave dne and em are the same thing, but 2 and 3 suggest dne
> and em are NOT.

The standard library module Relation.Nullary.Negation contains proofs
showing that excluded middle and double-negation elimination are
logically equivalent.

-- 
/NAD