Lemma isTRRGhomo_Branch_of_Branch_to_Branch {T : preZFS} (x : T) (y : Branch T x) : isTRRGhomo (Branch_of_Branch_to_Branch x y). Proof. split. - intros xx yy. simpl. split. -- intros P ; apply P. -- intros P ; apply P. - simpl. unfold Branch_of_Branch_to_Branch. unfold selfedge. simpl. apply total2_paths_equiv. destruct y as [y π]. simpl. exists (idpath y). apply propproperty. Qed.