open classical theorem dne {p : Prop} (h : ¬¬p) : p := or.elim (em p) (assume hp : p, hp) (assume hnp : ¬p, absurd hnp h)