proposition: Lemma logeq_if_both_false (P Q : hProp) : ¬P -> ¬Q -> ( P ⇔ Q ).
proof: Proof. intros np nq. split. - intros p. apply fromempty. exact (np p). - intros q. apply fromempty. exact (nq q). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions