---

Step * of Lemma tidentity_wf_for_mon_hom

∀[g:IMonoid]. (Id{|g|} ∈ MonHom(g,g))
BY
{ ((D 0) THENA Auto) 
THEN MemTypeCD THENA Auto }

1
1. g : IMonoid
⊢ Id{|g|} ∈ |g| ⟶ |g|

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  (Id\{|g|\}  \mmember{}  MonHom(g,g))


By

---

Latex:
((D  0)  THENA  Auto) 
THEN  MemTypeCD  THENA  Auto

---

Home Index