proposition: Lemma isTRRGhomo_Up_to_Up (T : Tree) (x : pr11 T) (y : pr11 (Up x)) : isTRRGhomo (Up_to_Up T x y).
proof: 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.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions