proposition: Theorem ZFS_Branch_is_ZFS (X : ZFS) (x : X) : hasuniquerepbranch (Branch X x).
proof: Proof. unfold hasuniquerepbranch. intros y z. rewrite -> (Branch_of_Branch_eq_Branch x y). rewrite -> (Branch_of_Branch_eq_Branch x z). intros p. set (π := pr2 X). simpl in π. set (τ := π (pr1 y) (pr1 z) p). apply total2_paths_equiv. exists τ. apply propproperty. 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