Definition carrier_subtype_to_contained_subtype (B : hsubtype A) : contained_subtype A. Proof. use make_contained_subtype. - intro x. exists (∑ (H : A x), B (x ,, H)). abstract ( apply isaproptotal2; intro; intros; apply propproperty ). - exact (λ x, pr1). Defined.