fact: Definition list_nil (A: hSet) : listset A := ops' (list_algebra A) nil_idx.
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Terms