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