Lemma fromBranch_hsubtype {T : preZFS} {x : T} {S : hsubtype (pr11 (preZFS_Branch T x))} {t :pr11 (preZFS_Branch T x)} (s : S t) : preZFS_Branch_hsubtype_tohsubtype T x S (pr1 t). Proof. unfold preZFS_Branch_hsubtype_tohsubtype. simpl. unfold ishinh_UU. intros P X. apply X. exists (pr2 t). apply s. Qed.