proposition: Lemma list_cons_dom_id (A: hSet) : dom (list_algebra A) cons_idx = dirprod A (dirprod (listset A) unit).
proof: Proof. reflexivity. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Terms