The derivation of the double negation of ET is in line 243 of https://hub.darcs.net/olf/haskell_for_mathematicians/browse/haskell_for_logicians.lhs Then use DN on that term, as Tom Smeding suggested. Olaf