---

Step * of Lemma grp_eq_sym

∀[g:DMon]. ∀[a,b:|g|].  a =b b = b =b a
BY
{ ((RepD  
THENM BLemma `iff_imp_equal_bool` 
THENM RW bool_to_propC 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:DMon].  \mforall{}[a,b:|g|].    a  =\msubb{}  b  =  b  =\msubb{}  a


By

---

Latex:
((RepD   
THENM  BLemma  `iff\_imp\_equal\_bool` 
THENM  RW  bool\_to\_propC  0)  THEN  Auto)

---

Home Index