Lemma islogeqassochconj {P Q R : hProp} : (P ∧ Q) ∧ R <-> P ∧ (Q ∧ R). 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.