fact: Definition signature : UU := ∑ (S: decSet) (O: hSet), O → list S × S.
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.DecSet UniMath.Combinatorics.MoreLists