---

Step * of Lemma mon_when_of_id

∀[g:IMonoid]. ∀[b:𝔹].  ((when b. e) = e ∈ |g|)
BY
{ ((SeqOnM  
[RepD 
;Unfold `mon_when` 0 
;OnVar `b' BoolCases 
;AbReduce 0 
;RW MonNormC 0]) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[b:\mBbbB{}].    ((when  b.  e)  =  e)


By

---

Latex:
((SeqOnM   
[RepD 
;Unfold  `mon\_when`  0 
;OnVar  `b'  BoolCases 
;AbReduce  0 
;RW  MonNormC  0])  THEN  Auto)

---

Home Index