proposition: Lemma islogeqcommhconj {P Q : hProp} : P ∧ Q <-> Q ∧ P.
proof: Proof. split. - intros PQ. exact (pr2 PQ,,pr1 PQ). - intros QP. exact (pr2 QP,,pr1 QP). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions