proposition: 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: Proof. unfold preZFS_Branch_hsubtype_tohsubtype. simpl. unfold ishinh_UU. intros P X. apply X. exists (pr2 t). apply s. Qed.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions