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