---

Step * of Lemma mon_when_swap

∀[g:Mon]. ∀[b,b':𝔹]. ∀[p:|g|].  ((when b. when b'. p) = (when b'. when b. p) ∈ |g|)
BY
{ ((SeqOnM  
[RepD 
;Unfold `mon_when` 0 
;AllBoolInd 
;AbReduce 0 
;RW MonNormC 0]) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:Mon].  \mforall{}[b,b':\mBbbB{}].  \mforall{}[p:|g|].    ((when  b.  when  b'.  p)  =  (when  b'.  when  b.  p))


By

---

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

---

Home Index