Lemma UpUpid (T : Tree) (x : pr11 T) (y : pr11 (Up x)) : pr1 (Up (pr1 y)) = Upw_to_TRRGraph (Up x) y. 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.