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