---

Step * of Lemma mon_when_true

∀[g:GrpSig]. ∀[b:𝔹]. ∀[x:|g|].  (when b. x) = x ∈ |g| supposing ↑b
BY
{ ((RepD 
THENM Unfold `mon_when` 0 
THENM SplitOnConclITE) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:GrpSig].  \mforall{}[b:\mBbbB{}].  \mforall{}[x:|g|].    (when  b.  x)  =  x  supposing  \muparrow{}b


By

---

Latex:
((RepD 
THENM  Unfold  `mon\_when`  0 
THENM  SplitOnConclITE)  THEN  Auto)

---

Home Index