Lemma isTRRGhomo_Up_to_Up (T : Tree) (x : pr11 T) (y : pr11 (Up x)) : isTRRGhomo (Up_to_Up T x y). Proof. split. - intros xx yy. simpl. split. -- intros P ; apply P. -- intros P ; apply P. - simpl. unfold Up_to_Up. unfold selfedge. simpl. apply total2_paths_equiv. destruct y as [y π]. simpl. assert (q : pr122 (pr221 T) x y y π (selfedge (pr1 T) y) = π). { apply propproperty. } rewrite -> q. exists (idpath (y ,, π)). apply propproperty. Qed.