Definition Up_to_Up (T : Tree) (x : pr11 T) (y : pr11 (Up x)) : pr1 (Upw_to_TRRGraph T (pr1 y)) → pr1 (Upw_to_TRRGraph (Up x) y). Proof. simpl. intros X. induction X as [t π]. induction y as [y σ]. exact ((t ,, ((pr122 (pr221 T)) x y t σ π)) ,, π). Defined.