Corollary reversal_LEM (P Q : hProp) : LEM -> (¬ P -> Q) -> (¬ Q -> P). Proof. intros lem f n. assert (g := negf f); clear f. assert (h := g n); clear g n. apply (dneg_LEM _ lem). exact h. Defined.
Require Import UniMath.MoreFoundations.Tactics.