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