Definition Branch_of_Branch_to_Branch {T : preZFS} (x : T) (y : Branch T x) : pr1 (Upw_to_TRRGraph (preZFS_Branch T x) y) → pr1 (Upw_to_TRRGraph (pr1 T) (pr1 y)). Proof. simpl. intros X. induction X as [[e ε] π]. simpl in e. simpl in π. unfold Upw_E in π. simpl in π. exact (e ,, π). Defined.