proposition: Lemma elem_sort_id (A: hSet) : support (list_algebra A) elem_sort_idx = A.
proof: Proof. reflexivity. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Terms