Lemma islogeqassochdisj {P Q R : hProp} : (P ∨ Q) ∨ R <-> P ∨ (Q ∨ R). Proof. split. - apply hinhuniv; intros hPQR. induction hPQR as [hPQ|hR]. + use (hinhuniv _ hPQ); clear hPQ; intros hPQ. induction hPQ as [hP|hQ]. * exact (hinhpr (ii1 hP)). * exact (hinhpr (ii2 (hinhpr (ii1 hQ)))). + exact (hinhpr (ii2 (hinhpr (ii2 hR)))). - apply hinhuniv; intros hPQR. induction hPQR as [hP|hQR]. + exact (hinhpr (ii1 (hinhpr (ii1 hP)))). + use (hinhuniv _ hQR); clear hQR; intros hQR. induction hQR as [hQ|hR]. * exact (hinhpr (ii1 (hinhpr (ii2 hQ)))). * exact (hinhpr (ii2 hR)). Defined.