proposition: Lemma hconj_absorb_hdisj (P Q : hProp) : (P ∧ (P ∨ Q)) = P.
proof: Proof. now apply hPropUnivalence; apply islogeqhconj_absorb_hdisj. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions