proposition: Lemma hfalse_hdisj (P : hProp) : (∅ ∨ P) = P.
proof: Proof. now apply hPropUnivalence; apply islogeqhfalse_hdisj. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions