proposition: Lemma cons_nil_id : list_cons = @cons.
proof: Proof. reflexivity. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Terms