fact: Definition listset (A: hSet): hSet := make_hSet (list A) (isofhlevellist 0 (setproperty A)).
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe