---

Step * of Lemma respects-equality-oalist1

∀[s:LOSet]. ∀[g:AbDMon].  respects-equality(|(s × (g↓set))| List;|oal(s;g)|)
BY
{ (Intros THEN (Unhide THENA Auto)) }

1
1. s : LOSet
2. g : AbDMon
⊢ respects-equality(|(s × (g↓set))| List;|oal(s;g)|)

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  (Unhide  THENA  Auto))

---

Home Index