proposition: Lemma islogeqcommhdisj {P Q : hProp} : hdisj P Q <-> hdisj Q P.
proof: Proof. intros. split. - simpl. apply hinhfun. apply coprodcomm. - simpl. apply hinhfun. apply coprodcomm. Defined.
imports: UniMath.Foundations.PartD