Corollary unique_exists {A : UU} {B : A -> UU} (x : A) (b : B x) (h : ∏ y, isaprop (B y)) (H : ∏ y, B y -> y = x) : iscontr (total2 (λ t : A, B t)). Proof. use make_iscontr. - exact (x,,b). - intros t. apply subtypePath. + exact h. + apply (H (pr1 t)). exact (pr2 t). Defined.