proposition: Lemma UpUpid (T : Tree) (x : pr11 T) (y : pr11 (Up x)) : pr1 (Up (pr1 y)) = Upw_to_TRRGraph (Up x) y.
proof: Proof. apply TRRGraph_univalence. exists (make_weq (Up_to_Up T x y) (isweq_Up_to_Up T x y)). apply (isTRRGhomo_Up_to_Up T 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