proposition: Lemma proofirrelevance (X : UU) : isaprop X -> isProofIrrelevant X.
proof: Proof. intros is x x'. unfold isaprop in is. unfold isofhlevel in is. exact (iscontrpr1 (is x x')). Defined.
imports: UniMath.Foundations.PartA