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