Lemma Branch_of_Branch_eq_Branch {T : preZFS} (x : T) (y : Branch T x) : Branch (Branch T x) y = Branch T (pr1 y). Proof. apply preZFS_univalence. unfold preZFS_iso. unfold Tree_iso. simpl. exact ((Branch_of_Branch_to_Branch x y ,, isweq_Branch_of_Branch_to_Branch x y) ,, isTRRGhomo_Branch_of_Branch_to_Branch x y). Qed.