---

Step * of Lemma id-is-monoid_hom

∀[A:GrpSig]. (λx.x ∈ MonHom(A,A))
BY
{ (((Unfold `monoid_hom` 0) THEN Auto) THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. A : GrpSig
⊢ IsMonHom{A,A}(λx.x)

---

Latex:

---

Latex:
\mforall{}[A:GrpSig].  (\mlambda{}x.x  \mmember{}  MonHom(A,A))


By

---

Latex:
(((Unfold  `monoid\_hom`  0)  THEN  Auto)  THEN  MemTypeCD  THEN  Auto)

---

Home Index