proposition: Lemma isTRRGhomo_Branch_of_Branch_to_Branch {T : preZFS} (x : T) (y : Branch T x) : isTRRGhomo (Branch_of_Branch_to_Branch x y).
proof: 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.
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