[Agda] (Stronger) double negation of law of excluded middle

[Dmytro Starosud]

Hello everyone

Could you have a look at my problem below?
I am trying to prove something that looks like just better double negation
of law of excluded middle:

¬¬lem : ¬ ¬ ((A : Set) → A ⊎ ¬ A)
¬¬lem = _

Which I cannot prove, whereas following one is pretty easy to prove:

¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)
¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))

Is it actually possible to prove the first one in constructive logic (in
particular in Agda)?

Thanks in advance for your help!

Best regards,
Dmytro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141011/58992e94/attachment.html