proposition: Corollary subtypeInjectivity_prop {A : UU} (B : A -> hProp) : ∏ (x y : total2 B), (x = y) ≃ (pr1 x = pr1 y).
proof: Proof. intros. apply subtypeInjectivity. intro. apply propproperty. Defined.
imports: UniMath.Foundations.PartD