Definition subtype_plus_in {X} {S:hsubtype X} {z:X} {T:hsubtype X} : S ⊆ T -> T z -> subtype_plus S z ⊆ T. Proof. intros le Tz x S'x. apply (squash_to_hProp S'x). intros [Sx|e]. - exact (le x Sx). - induction e. exact Tz. Defined.