proposition: Lemma path_to_ctr (A : UU) (B : A -> UU) (isc : ∃! a, B a) (a : A) (p : B a) : a = pr1 (pr1 isc).
proof: Proof. set (Hi := tpair _ a p). apply (maponpaths pr1 (pr2 isc Hi)). Defined.
imports: UniMath.Foundations.Preamble