proposition: Lemma ishom_nat_to_z2: @ishom _ nat_algebra z2_algebra (nat_to_z2).
proof: Proof. unfold ishom. intros. induction nm as [n proofn]. inductive_reflexivity n proofn. Defined.
imports: UniMath.Foundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.MoreLists UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Terms