proposition: Lemma islogeqhhtrue_hconj {P : hProp} : htrue ∧ P <-> P.
proof: Proof. split. - intros hP; apply (pr2 hP). - intros hP. split; [ apply tt | apply hP ]. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions