proposition: Lemma isaprop_assume_it_is {X : UU} : (X -> isaprop X) -> isaprop X.
proof: Proof. intros f. apply invproofirrelevance; intros x y. apply proofirrelevance. now apply f. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions