Theorem ZFS_Branch_is_ZFS (X : ZFS) (x : X) : hasuniquerepbranch (Branch X x). 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.