proposition: Corollary reversal_LEM (P Q : hProp) : LEM -> (¬ P -> Q) -> (¬ Q -> P).
proof: 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.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics