<div dir="ltr">Hello everyone<div><br></div><div>Could you have a look at my problem below?</div><div>I am trying to prove something that looks like just better double negation of law of excluded middle:</div><div><br></div><div><div>¬¬lem : ¬ ¬ ((A : Set) → A ⊎ ¬ A)</div><div>¬¬lem = _</div></div><div><br></div><div>Which I cannot prove, whereas following one is pretty easy to prove:</div><div><br></div><div><div>¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)</div><div>¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))</div></div><div><br></div><div>Is it actually possible to prove the first one in constructive logic (in particular in Agda)?<br></div><div><br></div><div>Thanks in advance for your help!</div><div><br></div><div>Best regards,</div><div>Dmytro</div><div><br></div></div>