proposition: Lemma Branch_of_Branch_eq_Branch {T : preZFS} (x : T) (y : Branch T x) : Branch (Branch T x) y = Branch T (pr1 y).
proof: 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.
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