proposition: Lemma sigT_UIP {A: HSet} {B: A -> HSet} (x y: {a: A & B a}) (p q: x = y): p = q.
proof: Proof. unshelve eapply sigT_decompose. now apply A. now apply (B y.1). Qed.
imports: Logic.FunctionalExtensionality Logic.Eqdep_dec Bonak(Notation)