Definition Up_to_Up_inv (T : Tree) (x : pr11 T) (y : pr11 (Up x)) : pr1 (Upw_to_TRRGraph (Up x) y) → pr1 (Upw_to_TRRGraph T (pr1 y)). Proof. simpl. intros X. induction X as [t π]. induction y as [y σ]. induction t as [tt θ]. simpl. unfold Upw_E in π. simpl in π. exact (tt ,, π). Defined.