Lemma Branch_to_subtype (T : preZFS) (x : T) (S : hsubtype (pr11 (preZFS_Branch T x))) : hsubtype_to_preZFS_Branch_hsubtype T x (preZFS_Branch_hsubtype_tohsubtype T x S) = S. Proof. set (H := (hsubtype_to_preZFS_Branch_hsubtype T x (preZFS_Branch_hsubtype_tohsubtype T x S))). apply (funextfunPreliminaryUAH univalenceAxiom (pr11 (preZFS_Branch T x)) hProp H S). unfold homot. intros y. unfold preZFS_Branch_hsubtype_tohsubtype. unfold hsubtype_to_preZFS_Branch_hsubtype. simpl. assert (ES : ((∃ e : Ed T x (pr1 y), S (pr1 y,, e)) ∧ Ed T x (pr1 y)) -> S y). { intros X. destruct X as [ε e]. apply (ε (S y)). intros X. destruct y. destruct X as [y z]. simpl in z. simpl in y. assert ( p : y = pr2 ). apply propproperty. rewrite <- p. apply z. } assert (SE : ((∃ e : Ed T x (pr1 y), S (pr1 y,, e)) ∧ Ed T x (pr1 y)) <- S y). { intros X. simpl. unfold ishinh_UU. split. - intros P Q. apply Q. exists (pr2 y). apply X. - apply (pr2 y). } apply (hPropUnivalence ((∃ e : Ed T x (pr1 y), S (pr1 y,, e)) ∧ Ed T x (pr1 y)) (S y) ES SE). Qed.