proposition: Corollary isaprop_total2 (X : hProp) (Y : X -> hProp) : isaprop (∑ x, Y x).
proof: Proof. intros. apply (isofhleveltotal2 1). - apply propproperty. - intro x. apply propproperty. Defined.
imports: UniMath.Foundations.PartD