---

Step * of Lemma respects-equality-oalist2

∀[s:LOSet]. ∀[g:AbDMon].  respects-equality((|s| × |g|) List;|oal(s;g)|)
BY
{ (InstLemma `respects-equality-oalist1` []
   THEN RepeatFor 2 (ParallelLast')
   THEN NthHypSq (-1)
   THEN Auto
   THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[s:LOSet].  \mforall{}[g:AbDMon].    respects-equality((|s|  \mtimes{}  |g|)  List;|oal(s;g)|)


By

---

Latex:
(InstLemma  `respects-equality-oalist1`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  NthHypSq  (-1)
  THEN  Auto
  THEN  Computation)

---

Home Index