proposition: Lemma toBranch_hsubtype {T : preZFS} {x : T} {S : hsubtype (pr111 T)} {t : pr111 T} (e : Ed T x t) (s : S t) : hsubtype_to_preZFS_Branch_hsubtype T x S (t ,, e).
proof: Proof. unfold hsubtype_to_preZFS_Branch_hsubtype. simpl. split. apply s. apply e. 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