Yes, thank you, I made some stupid mistakes there. I find the last one slightly clearer if you change the argument order: DNimpliesLEM : ((x:Type) -> DN x

Yes, thank you, I made some stupid mistakes there. I find the last one slightly clearer if you change the argument order: DNimpliesLEM : ((x:Type) -> DN x) -> ((y:Type) -> LEM y) DNimpliesLEM dn y = dn (LEM y) (notnotLEMproof y) Although with the original formulation you could prove the slightly stronger version: DNimpliesLEM : (x:Type) -> DN (LEM x) -> LEM x DNimpliesLEM x dn = dn (notnotLEMproof x) so that you don't need DN z to be true for all z, but just on the z you need (i.e. z = LEM x). It was an interesting exercise, and I learned a lot. First I tried proving (((x:Type) -> LEM x) -> _|_ ->) _|_ to then apply double negation directly to this, but this is actually not possible (as far as I can see). The double negation needs to be inside the quantifier. Maybe you can even write it simply like this with implicit parameters: DNimpliesLEM : DN (LEM x) -> LEM x DNimpliesLEM dn = dn notnotLEMproof