proposition: Lemma proof_by_contradiction {P:hProp} : LEM -> ¬ ¬ P -> P.
proof: Proof. intro lem. exact (decidable_proof_by_contradiction (lem P)). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions