proposition: Lemma hdisj_impl_2 {P Q : hProp} : P∨Q -> (P->Q) -> Q.
proof: Proof. intros o f. apply (squash_to_hProp o). intros [p|q]. - exact (f p). - exact q. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions