proposition: Lemma islogeqhdisj_absorb_hconj {P Q : hProp} : P ∨ (P ∧ Q) <-> P.
proof: Proof. split. - apply hinhuniv; intros hPPQ. induction hPPQ as [hP|hPQ]. + exact hP. + exact (pr1 hPQ). - intros hP; apply (hinhpr (ii1 hP)). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions