proposition: Lemma ishinh_irrel {X:UU} (x:X) (x':∥X∥) : hinhpr x = x'.
proof: Proof. apply proofirrelevance. apply propproperty. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions