Lemma contained_subtype_to_carrier_subtype_to_contained_subtype (B : contained_subtype A) : carrier_subtype_to_contained_subtype (contained_subtype_to_carrier_subtype B) = B. Proof. apply contained_subtype_eq. - intros x H. exact (pr2 H). - intros x H. exists (pr2 B x H). exact H. Qed.