---

Step * 1 of Lemma id-is-monoid_hom

.....set predicate..... 
1. A : GrpSig
⊢ IsMonHom{A,A}(λx.x)
BY
{ RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto)) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  A  :  GrpSig
\mvdash{}  IsMonHom\{A,A\}(\mlambda{}x.x)


By

---

Latex:
RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto))

---

Home Index