proposition: Lemma uniqueExists {A : UU} {P : A -> UU} {a b : A} (Hexists : ∃! a, P a) (Ha : P a) (Hb : P b) : a = b.
proof: Proof. assert (H : tpair _ _ Ha = tpair _ _ Hb). { now apply proofirrelevancecontr. } exact (base_paths _ _ H). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions