fact: Definition selfedge (G : TRRGraph) (x : pr1 G) : pr1 (pr2 G) x x := (pr1 (pr2 (pr2 (pr2 G))) x).
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