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