proposition: Lemma logeq_if_both_true (P Q : hProp) : P -> Q -> ( P ⇔ Q ).
proof: Proof. intros p q. split. - intros _. exact q. - intros _. exact p. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions